Fixed-Point Methods in Parametric Model Checking
作者： Michał Knapik , Wojciech Penczek
DOI: 10.1007/978-3-319-11313-5_22
关键词: Computer science 、 Deadlock 、 Theoretical computer science 、 Parametric model 、 Parametric Image 、 Reachability 、 Linear temporal logic 、 Modal logic 、 Computation tree logic 、 Fixed point
摘要: We present a general framework for the synthesis of constraints under which selected properties hold in class models with discrete transitions, together Boolean encoding - based method implementing theory. introduce notions parametric image and preimage, show how to use them build fixed-point algorithms model checking reachability deadlock freedom. An outline ideas shown this paper were specialized an extension Computation Tree Logic is given some experimental results.
springer.com
sci-hub.st 参考文章(26)
Malik Ghallab, Dana S. Nau, Paolo Traverso, Automated Planning, Theory And Practice ,(2006)
Doron Peled, All from One, One for All: on Model Checking Using Representatives computer aided verification. pp. 409- 423 ,(1993) , 10.1007/3-540-56922-7_34
Véronique Bruyère, Emmanuel Dall’Olio, Jean-FranÇois Raskin, Durations, Parametric Model-Checking in Timed Automata with Presburger Arithmetic symposium on theoretical aspects of computer science. pp. 687- 698 ,(2003) , 10.1007/3-540-36494-3_60
Francesco Belardinelli, Andrew V. Jones, Alessio Lomuscio, Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata Fundamenta Informaticae. ,vol. 112, pp. 19- 37 ,(2011) , 10.3233/FI-2011-576
Barbara Di Giampaolo, Salvatore La Torre, Margherita Napoli, Parametric Metric Interval Temporal Logic Language and Automata Theory and Applications. pp. 249- 260 ,(2010) , 10.1007/978-3-642-13089-2_21
Edmund M. Clarke, The Birth of Model Checking 25 Years of Model Checking. pp. 1- 26 ,(2008) , 10.1007/978-3-540-69850-0_1
Michał Knapik, Maciej Szreter, Wojciech Penczek, Bounded parametric model checking for elementary net systems Lecture Notes in Computer Science. ,vol. 4, pp. 42- 71 ,(2010) , 10.1007/978-3-642-18222-8_3
Wojciech Penczek, Agata Pòłrola, Andrzej Zbrzezny, SAT-based (parametric) reachability for a class of distributed time Petri nets Lecture Notes in Computer Science. ,vol. 4, pp. 72- 97 ,(2010) , 10.1007/978-3-642-18222-8_4
Farn Wang, Parametric Analysis of Computer Systems formal methods. ,vol. 17, pp. 39- 60 ,(2000) , 10.1023/A:1008782501688
Charles Pecheur, Franco Raimondi, Symbolic Model Checking of Logics with Actions Model Checking and Artificial Intelligence. pp. 113- 128 ,(2007) , 10.1007/978-3-540-74128-2_8