Some Results on the Verification of Recursive Parallel Systems

Relatore
Massimo Benerecetti - Universita' di Napoli
Data e ora
martedì 10 febbraio 2004 alle ore 17.30
Luogo
Ca' Vignal - Piramide, Piano 0, Sala Verde
Referente
Maria Paola Bonacina
Referente esterno
Data pubblicazione
24 gennaio 2004
Dipartimento
 

Riassunto

Process Rewriting Systems (PRS) is a well known formal settingsuitable for describing relevant classes of infinite state systemswith recursion and/or parallelism. For instance, both PushdownAutomata and Petri Nets can be accommodated in the framework, as wellas various restricted combinations of them. For general PRSdecidability results are mainly limited to reachabilityproperties. The talk will focus on the problem of proving propertiesof infinite behaviors for a meaningful fragment of PRS, where bothrecursion and parallelism are allowed. Some decidability results fora class of properties about infinite derivations (namely, infiniteterm rewritings) in a PRS is provided. It will also be shown howthose results can be exploited for the verification of a small classof linear time properties of infinite state systems described by PRSs.





© 2002 - 2021  Universit√† degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234