Michał Knapik
Abstract
The article introduces a parametric extension of Action-Restricted Computation Tree Logic called pmARCTL. A symbolic fixed-point algorithm providing a solution to the exhaustive parameter synthesis problem is proposed. The parametric approach allows for an in-depth system analysis and synthesis of the correct parameter values. The time complexity of the problem and the algorithm is provided. An existential fragment of pmARCTL (pmEARCTL) is identified, in which all of the solutions can be generated from a minimal and unique base. A method for computing this base using symbolic methods is provided. The prototype tool SPATULA implementing the algorithm is applied to the analysis of three benchmarks: faulty Train-Gate-Controller, Peterson’s mutual exclusion protocol, and a generic pipeline processing network. The experimental results show efficiency and scalability of our approach compared to the naive solution to the problem.
- R. Alur, K. Etessami, S. La Torre, and D. Peled. 2001. Parametric temporal logic for “model measuring.” ACM Transactions on Computational Logic 2, 3, 388--407. Google Scholar
Digital Library
- R. Alur, T. Henzinger, and M. Vardi. 1993. Parametric real-time reasoning. In Proceedings of the 25th Annual Symposium on Theory of Computing. ACM, New York, NY, 592--601. Google ScholarDigital Library
- É. André, L. Fribourg, U. Kühne, and R. Soulat. 2012. IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In FM 2012: Formal Methods. Lecture Notes in Computer Science, Vol. 7436. Springer, 33--36.Google Scholar
- C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press, Cambridge, MA. Google ScholarDigital Library
- F. Belardinelli, A. V. Jones, and A. Lomuscio. 2011. Model checking temporal-epistemic logic using alternating tree automata. Fundamenta Informaticae: Concurrency Specification and Programming 112, 1, 19--37. Google ScholarDigital Library
- V. Bruyére, E. Dall’Olio, and J. Raskin. 2008. Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic 9, 2, 1--23. Google ScholarDigital Library
- E. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons for branching-time temporal logic. In Logics of Programs. Lecture Notes in Computer Science, Vol. 131. Springer, 52--71. Google ScholarDigital Library
- A. Classen, P. Heymans, P.-Y. Schobbens, and A. Legay. 2011. Symbolic model checking of software product lines. In Proceedings of the 33rd International Conference on Software Engineering (ICSE’11). ACM, New York, NY, 321--330. Google ScholarDigital Library
- O. Coudert, J. C. Madre, H. Fraisse, and H. Touati. 1993. Implicit prime cover computation: An overview. In Proceedings of the Synthesis and Simulation Meeting and International Interchange (SASIMI’93).Google Scholar
- C. Daskalakis, R. M. Karp, E. Mossel, S. Riesenfeld, and E. Verbin. 2011. Sorting and selection in posets. SIAM Journal on Computing 40, 3, 597--622. Google ScholarDigital Library
- B. Di Giampaolo, S. La Torre, and M. Napoli. 2010. Parametric metric interval temporal logic. In Language and Automata Theory and Applications. Lecture Notes in Computer Science, Vol. 6031. Springer, 249--260. Google ScholarDigital Library
- J. Goldsmith, M. Hagen, and M. Mundhenk. 2008. Complexity of DNF minimization and isomorphism testing for monotone formulas. Information and Computation 206, 6, 760--775. Google ScholarDigital Library
- T. Hune, J. Romijn, M. Stoelinga, and F. Vaandrager. 2002. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52--53, 183--220.Google ScholarCross Ref
- A. V. Jones, M. Knapik, A. Lomuscio, and W. Penczek. 2012. Group synthesis for parametric temporal-epistemic logic. In Proceedings of the 11th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’12). 1107--1114. Google ScholarDigital Library
- G. Katz and D. Peled. 2010. Code mutation in verification and automatic code correction. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, Vol. 6015. Springer, 435--450. Google ScholarDigital Library
- M. Knapik. 2014. SPATULA, Simple Parametric Verification Tool. Retrieved August 10, 2015, from https://michalknapik.github.io/spatula.Google Scholar
- M. Knapik, A. Męski, and W. Penczek. 2014. Action synthesis for branching time logic: Theory and applications. In Proceedings of the 14th International Conference on Application of Concurrency to System Design (ACSD’14). IEEE, Los Alamitos, CA, 1--10. Google ScholarDigital Library
- C. Pecheur and F. Raimondi. 2006. Symbolic model checking of logics with actions. In Model Checking and Artificial Intelligence. Lecture Notes in Computer Science, Vol. 4428. Springer, 113--128. Google ScholarDigital Library
- D. Peled. 1993. All from one, one for all: On model checking using representatives. In Computer Aided Verification. Lecture Notes in Computer Science, Vol. 697. Springer, 409--423. Google ScholarDigital Library
- G. L. Peterson. 1981. Myths about the mutual exclusion problem. Information Processing Letters 12, 3, 115--116.Google ScholarCross Ref
- W. Quine. 1952. The problem of simplifying truth functions. American Mathematical Monthly 59, 8, 521--531.Google ScholarCross Ref
- P. Schnoebelen. 2002. The complexity of temporal logic model checking. In Advances in Modal Logic, Vol. 4. World Scientific Publishing, 393--436.Google Scholar
- F. Somenzi. 2012. CUDD: CU Decision Diagram Package. Retrieved August 10, 2015, from http://vlsi.colorado.edu/∼fabio/CUDD/cuddIntro.html.Google Scholar
Index Terms
- Action Synthesis for Branching Time Logic: Theory and Applications
Recommendations
Action Synthesis for Branching Time Logic: Theory and Applications
ACSD '14: Proceedings of the 2014 14th International Conference on Application of Concurrency to System DesignWe introduce a parametric extension of Action-Restricted Computation Tree Logic. A symbolic fixed-point algorithm providing a solution to the exhaustive parameter synthesis problem is proposed. The parametric approach allows for an in-depth system ...
Distributed parametric model checking timed automata under non-Zenoness assumption
AbstractModel checking timed systems may be negatively impacted by the presence of Zeno runs as counterexamples. Such runs contain an infinite number of discrete actions occurring in a finite time, which is unrealistic; therefore, these runs must be ...
Parameter synthesis for polynomial biological models
HSCC '14: Proceedings of the 17th international conference on Hybrid systems: computation and controlParameter determination is an important task in the development of biological models. In this paper we consider parametric polynomial dynamical systems and address the following parameter synthesis problem: find a set of parameter values so that the ...
Comments