Action Synthesis for Branching Time Logic: Theory and Applications

• Published in: ACM transactions on embedded computing systems 2015-12, Vol.14 (4), p.1-23, Article 64
• Main Authors: Knapik, Michał, Męski, Artur, Penczek, Wojciech
• Format: Article
• Language: English
• Subjects: Cross-computing tools and techniques; Formal methods; Formal software verification; General and reference; Program reasoning; Program verification; Semantics and reasoning; Software and its engineering; Software creation and management; Software development process management; Software functional properties; Software organization and properties; Software verification; Software verification and validation; Theory of computation; Verification
• ISSN: 1539-9087; 1558-3465
• DOI: 10.1145/2746337

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.