Action Synthesis for Branching Time Logic: Theory and Applications

We 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 analysis and synthesis of correct parameter values. The time complexity of the problem and of the algorithm 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 in comparison with a naive solution to the problem.