Refinement checking on parametric modal transition systems Journal Article

Author(s): Beneš, Nikola; Křetínský, Jan; Larsen, Kim G; Möller, Mikael H; Sickert, Salomon; Srba, Jiří
Article Title: Refinement checking on parametric modal transition systems
Affiliation IST Austria
Abstract: Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.
Keywords: model checking; Reactive system; State of the art; Modal Transition Systems; Boolean functions; Degree of nondeterminism; Direct encoding; Quantified Boolean formulas; Refinement checking; Refinement process
Journal Title: Acta Informatica
Volume: 52
Issue 2-3
ISSN: 1432-0525
Publisher: Springer  
Date Published: 2015-04-01
Start Page: 269
End Page: 297
DOI: 10.1007/s00236-015-0215-4
Notes: The research leading to the results in this article has received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement Nr. 318490 (SENSATION) and Grant Agreement Nr. 601148 (CASSTING), from the Sino-Danish Basic Research Center IDEA4CPS funded by the Danish National Research Foundation and the National Science Foundation China. The research was further funded in part by the European Research Council (ERC) under the Grant Agreement 267989 (QUAREM), by the Austrian Science Fund (FWF) project S11402-N23 (RiSE) and by the Czech Science Foundation Grant No. P202/12/G061. Nikola Beneš has been supported by the MEYS Project No. CZ.1.07/2.3.00/30.0009 Employment of Newly Graduated Doctors of Science for Scientific Excellence.
Open access: no
IST Austria Authors
Related IST Austria Work