We define extensions of CTL and TCTL with strategic operators, called Strategic CTL (SCTL) and Strategic TCTL (STCTL), respectively. For each of the above logics we give a synchronous and asynchronous semantics, ie STCTL is interpreted over networks of extended Timed Automata (TA) that either make synchronous moves or synchronise via joint actions. We consider several semantics regarding information: imperfect (i) and perfect (I), and recall: imperfect (r) and perfect (R). We prove that SCTL is more expressive than ATL for all semantics, and this holds for the timed versions as well. Moreover, the model checking problem for STCTLir is of the same complexity as for ATLir, the model checking problem for STCTLir is of the same complexity as for TCTL, while for STCTLiR it is undecidable as for ATLiR. The above results suggest to use STCTLir and STCTLir in practical applications. Therefore, we use the tool IMITATOR to support model checking of STCTLir.

International audience

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.

Expressing attack-defence trees in a multiagent setting allows for studying a new aspect of security scenarios, namely, how the number of agents and their task assignment impact the performance,e.g.,attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a nontrivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesizes such an assignment, targeting minimal attack time and using the minimal number of agents for a given attack-defence tree. We also investigate an alternative approach for the same problem using rewriting logic, starting with a simple and elegant declarative model, whose correctness (in terms of schedule's optimality) is self-evident. We then refine this specification, inspired by the design of our specialized algorithm, to obtain an efficient system that can be used as a playground to explore various aspects of attack-defence trees. We compare the two approaches on different benchmarks.

Expressing attack-defence trees in a multi-agent setting allows for studying a new aspect of security scenarios, namely how the number of agents and their task assignment impact the performance, e.g. attack time, of strategies executed by opposing coalitions. Optimal scheduling of agents' actions, a non-trivial problem, is thus vital. We discuss associated caveats and propose an algorithm that synthesises such an assignment, targeting minimal attack time and using minimal number of agents for a given attack-defence tree.

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems (MAS), together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

We propose a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information. Based on the semantics, we show some general complexity results for verification of strategic abilities in asynchronous interaction. More importantly, we develop a methodology for partial order reduction in verification of agents with imperfect information. We show that the reduction preserves an important subset of strategic properties, with as well as without the fairness assumption. We also demonstrate the effectiveness of the reduction on a number of benchmarks. Interestingly, the reduction does not work for strategic abilities under perfect information.

In earlier work, we presented translations of attack-defence trees (ADTrees) to extended asynchronous multi-agent systems. By avoiding some sequences, agent models constructed via these transformations already embed state space reductions. Here, we introduce Guarded Update Systems and their synchronisation topology, allowing us to define a new general reduction scheme that applies to tree topologies, and in particular to ADTrees. The reduction exploits the layered structure of a tree by avoiding unnecessary interleavings between nodes at different depths. We prove the soundness of this new method and present extensive experimental results, including scalable models, to demonstrate it can be effectively used alongside previously employed techniques.

We present nine SAT-solvers and compare their efficiency for several decision and combinatorial problems: three classical NP-complete problems of the graph theory, bounded Post correspondence problem (BPCP), extended string correction problem (ESCP), two popular chess problems, PSPACE-complete veri fication of UML systems, and the Towers of Hanoi (ToH) of exponential solutions. In addition to several known reductions to SAT for the problems of graph k-colouring, vertex k-cover, Hamiltonian path, and verification of UML systems, we also define new original reductions for the N-queens problem, the knight’s tour problem, and ToH, SCP, and BPCP. Our extensive experimental results allow for drawing quite interesting conclusions on efficiency and applicability of SAT-solvers to different problems: they behave quite efficiently for NP-complete and harder problems but they are by far inferior to tailored algorithms for specific problems of lower complexity.