In the formal verification of software systems, modelchecking is one of the most studied and applied techniques. Systems represented by mathematical models are checked against properties expressed as logical formulae. When the subjects of the verification are concurrent and distributed systems, models and specification logics capable of faithfully capturing the concurrent features of computations, like causal dependency and independence between actions of the systems, can sometimes be convenient or even essential. In this thesis we study the foundations of the modelchecking problem in a logic for true concurrency, whose formulae predicate over executability of actions in computations and their causality and concurrency relations. The logic represents the logical counterpart of historypreserving bisimilarity, a popular behavioural equivalence in the true concurrent spectrum and one of the strongest known to be decidable. It includes least and greatest fixpoint operators in mucalculus style, making it able to express properties of infinite computations. The logic is interpreted over event structures, a classical semantic model for true concurrency, that describes the behaviour of systems in terms of the events that can occur in computations and the causal dependencies and conflicts between them. It can be naturally used over any operational model that admits a causal semantic. Of particular interest, here, will be Petri nets. They are a widely adopted operational model allowing for a natural representation of concurrent and distributed systems. We prove that the modelchecking problem is decidable over a class of event structures satisfying a suitable regularity condition, and provide three decision procedures based on three different approaches. Along the lines of some classical work for the modal mucalculus, we first develop a local modelchecker in the form of a tableau system, for which we prove termination, soundness and completeness. The tableau system allows for a clean and intuitive proof of decidability, but a direct implementation of the procedure can be extremely inefficient. On the way to a practical implementation, we then present an automatabased modelchecking technique. Given a formula and a model, a parity tree automaton is constructed whose language is nonempty if and only if the model satisfies the formula. The automaton is usually infinite. We discuss how it can be quotiented to a finite automaton preserving its language via a suitable equivalence over its states. We show how the method instantiates on finite safe Petri nets, where such equivalence can be effectively computed. Finally, we devise a general gametheoretic approach to the solution of systems of fixpoint equations over a wide class of lattices. This applies, in principle, to a multitude of verification tasks, which reduce to the computation of fixpoints of monotone functions. Being an instance of those tasks, we show how the method can be instantiated and applied to the modelchecking problem of interest in the thesis.
Tableaux, automata and games for true concurrency properties / Padoan, Tommaso.  (2019 Dec 02).
Tableaux, automata and games for true concurrency properties
Padoan, Tommaso
2019
Abstract
In the formal verification of software systems, modelchecking is one of the most studied and applied techniques. Systems represented by mathematical models are checked against properties expressed as logical formulae. When the subjects of the verification are concurrent and distributed systems, models and specification logics capable of faithfully capturing the concurrent features of computations, like causal dependency and independence between actions of the systems, can sometimes be convenient or even essential. In this thesis we study the foundations of the modelchecking problem in a logic for true concurrency, whose formulae predicate over executability of actions in computations and their causality and concurrency relations. The logic represents the logical counterpart of historypreserving bisimilarity, a popular behavioural equivalence in the true concurrent spectrum and one of the strongest known to be decidable. It includes least and greatest fixpoint operators in mucalculus style, making it able to express properties of infinite computations. The logic is interpreted over event structures, a classical semantic model for true concurrency, that describes the behaviour of systems in terms of the events that can occur in computations and the causal dependencies and conflicts between them. It can be naturally used over any operational model that admits a causal semantic. Of particular interest, here, will be Petri nets. They are a widely adopted operational model allowing for a natural representation of concurrent and distributed systems. We prove that the modelchecking problem is decidable over a class of event structures satisfying a suitable regularity condition, and provide three decision procedures based on three different approaches. Along the lines of some classical work for the modal mucalculus, we first develop a local modelchecker in the form of a tableau system, for which we prove termination, soundness and completeness. The tableau system allows for a clean and intuitive proof of decidability, but a direct implementation of the procedure can be extremely inefficient. On the way to a practical implementation, we then present an automatabased modelchecking technique. Given a formula and a model, a parity tree automaton is constructed whose language is nonempty if and only if the model satisfies the formula. The automaton is usually infinite. We discuss how it can be quotiented to a finite automaton preserving its language via a suitable equivalence over its states. We show how the method instantiates on finite safe Petri nets, where such equivalence can be effectively computed. Finally, we devise a general gametheoretic approach to the solution of systems of fixpoint equations over a wide class of lattices. This applies, in principle, to a multitude of verification tasks, which reduce to the computation of fixpoints of monotone functions. Being an instance of those tasks, we show how the method can be instantiated and applied to the modelchecking problem of interest in the thesis.File  Dimensione  Formato  

padoan_tommaso_tesi.pdf
accesso aperto
Tipologia:
Tesi di dottorato
Licenza:
Non specificato
Dimensione
1.54 MB
Formato
Adobe PDF

1.54 MB  Adobe PDF  Visualizza/Apri 
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.