Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 14:15 - 14:40 at Sala VII - Algebra, Coalgebra, Model Checking Chair(s): Barbara König

We study the model-checking problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal dependencies. The logic, that represents the logical counterpart of history-preserving bisimilarity, is naturally interpreted over event structures or any formalism which can be given a causal semantics, like Petri nets. It includes least and greatest fixpoint operators and thus it can express properties of infinite computations. Since the event structure associated with a system is typically infinite (even if the system is finite state), already the decidability of model-checking is non-trivial.

Along the lines of some classical work for the modal mu-calculus, we first develop a local model-checking technique based on a tableau system, for which, over a class of event structures satisfying a suitable regularity condition, referred to as strong regularity, 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.

For easing the development of a more efficient model-checking technique, we move to an automata-theoretic framework. Given a formula and a strongly regular event structure, we show how to construct a parity tree automaton whose language is non-empty if and only if the event structure satisfies the formula. The automaton is usually infinite. We discuss how it can be quotiented to an equivalent finite automaton, where emptiness can be checked effectively. In order to show the applicability of the approach, we discuss how it instantiates to finite safe Petri nets, providing also a corresponding proof-of-concept model-checking tool.

Slides (opct19.pdf)219KiB

Tue 15 Jan

13:50 - 15:30: OPCT 2019 - Algebra, Coalgebra, Model Checking at Sala VII
Chair(s): Barbara KönigUniversity of Duisburg-Essen
opct-2019-papers13:50 - 14:15
Joost-Pieter KatoenRWTH Aachen University
File Attached
opct-2019-papers14:15 - 14:40
Paolo BaldanUniversity of Padova
File Attached
opct-2019-papers14:40 - 15:05
Helle Hvid HansenDelft University of Technology
File Attached
opct-2019-papers15:05 - 15:30
Simone TiniUniversity of Insubria