Laure Petrucci

IMITATOR4AMAS supports model checking and synthesis of memoryless imperfect information strategies for STCTL, interpreted over networks of parametric timed automata with asynchronous execution. While extending the verifier IMITATOR, IMITATOR4AMAS is the first tool for strategy synthesis in this setting. Our experimental results show a substantial speedup over previous approaches.

We present a (semi)-algorithm to compute winning strategies for parametric timed games. Previous algorithms only synthesized constraints on the clock parameters for which the game is winning. A new definition of (winning) strategies is proposed, and ways to compute them. A transformation of these strategies to (parametric) timed automata allows for building a controller enforcing them. The feasibility of the method is demonstrated by an implementation and experiments for the Production Cell case study.

Model checking of temporal logics in a well established technique to verify and validate properties of multi-agent systems (MAS). However, practical model checking requires input models of manageable size. In this paper, we extend the model reduction method by variable-based abstraction, proposed recently by Jamroga and Kim, to the verification of real-time systems and properties. To this end, we define a real-time extension of MAS graphs, extend the abstraction procedure, and prove its correctness for the universal fragment of Timed Computation Tree Logic (TCTL). Besides estimating the theoretical complexity gains, we present an experimental evaluation for a simplified model of the Estonian voting system and verification using the Uppaal model checker.

Strategic Timed CTL (STCTL) is an expressive logic that integrates branching time CTL with the representation of continuous time, and the notion of strategic abilities of agents. This makes STCTL suitable for specifying properties of asynchronous multi-agent systems modeled as networks of Parametric Timed Automata (PTA). Existing model checkers and synthesis procedures for STCTL are often limited in scope (bounded analyses), rely on ad-hoc implementations, and are difficult to prove correct. In this paper we propose declarative methods for STCTL model checking and synthesis using rewriting logic. Our approach uses rewriting modulo SMT to represent clock constraints and timed parameters as terms in a rewrite theory, and we adequately capture the continuous semantics of STCTL via rewriting strategies. The resulting algebraic specification is executable in the rewrite engine Maude. This is a novel application of Maude’s strategy language and, since our procedures are grounded on logical means, it is simpler to prove them correct. Our approach advances the state of the art for the analysis of multi-agent systems by allowing for the nesting of temporal operators and universal STCTL formulas, which have not been considered before. We benchmark our rewrite theory against existing procedures for STCTL, demonstrating competitive performance and even outperforming dedicated procedures for the existential fragment of STCTL. We thus provide a more robust and verifiable approach to STCTL model checking and synthesis.