Curriculum
Computer Science and Innovation for Societal Challenges, XXXII series
Grant sponsor
UNIPD
Supervisor

Paolo Baldan
Co-supervisor
Sara Mondini

Project: Tableaux, automata and games for true concurrency properties.
Full text of the dissertation book can be downloaded from: http://paduaresearch.cab.unipd.it/12796/ description

Abstract: In the formal verification of software systems, model-checking 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 model-checking 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 history-preserving 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 mu-calculus 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 model-checking 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 mu-calculus, we first develop a local model-checker 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 automata-based model-checking technique. Given a formula and a model, a parity tree automaton is constructed whose language is non-empty 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 game-theoretic 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 model-checking problem of interest in the thesis.