Parameterized model checking of rendezvous systems Conference Paper

Author(s): Aminof, Benjamin; Kotek, Tomer; Rubin, Sacha; Spegni, Francesco; Veith, Helmut
Title: Parameterized model checking of rendezvous systems
Title Series: LNCS
Affiliation IST Austria
Abstract: A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata.
Conference Title: CONCUR: Concurrency Theory
Volume: 8704
Conference Dates: September 2-5, 2014
Conference Location: Rome, Italy
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Date Published: 2014-09-01
Start Page: 109
End Page: 124
DOI: 10.1007/978-3-662-44584-6_9
Notes: The second, third, fourth and fifth authors were supported by the Austrian National Research Network S11403-N23 (RiSE) of the Austrian Science Fund (FWF) and by the Vienna Science and Technology Fund (WWTF) through grants PROSEED, ICT12-059, and VRG11-005.
Open access: no
IST Austria Authors
  1. Sasha Rubin
    2 Rubin
  2. Benjamin Aminof
    1 Aminof
Related IST Austria Work