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.

Abstract Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environment and depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations “in the limit”.

This paper presents a concrete and a symbolic rewriting logic semantics for parametric time Petri nets with inhibitor arcs (PITPNs), a flexible model of timed systems where parameters are allowed in firing bounds. We prove that our semantics is bisimilar to the “standard” semantics of PITPNs. This allows us to use the rewriting logic tool Maude, combined with SMT solving, to provide sound and complete formal analyses for PITPNs. We develop and implement a new general folding approach for symbolic reachability, so that Maude-with-SMT reachability analysis terminates whenever the parametric state-class graph of the PITPN is finite. Our work opens up the possibility of using the many formal analysis capabilities of Maude—including full LTL model checking, analysis with user-defined execution strategies, and even statistical model checking—for such nets. We illustrate this by explaining how almost all formal analysis and parameter synthesis methods supported by the state-of-the-art PITPN tool Roméo can be performed using Maude with SMT. In addition, we also support analysis and parameter synthesis from parametric initial markings, as well as full LTL model checking and analysis with user-defined execution strategies. Experiments show that our methods outperform Roméo in many cases.

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.

As exascale platforms are in sight, high-performance computing needs to take failures into account and provide fault-tolerant applications and environments. Checkpoint-restart approaches do not require modifying the application, but are expensive at large scale. Application-based fault tolerance is more specific to the application and is expected to achieve better performance. In this paper, we address fault-tolerant matrix factorization with algorithms that present good performance, both during failure-free executions and when failures happen. A challenge when designing fault-tolerant algorithms is to make sure they are resilient to any failure scenario. Therefore, we design a model for these algorithms and prove they can tolerate failures at any moment, as long as enough processes are still alive.

The inherent computational complexity of validating and verifying concurrent systems implies a need to be able to exploit parallel and distributed computing architectures. We present a new distributed algorithm for state space exploration of concurrent systems on computing clusters. Our algorithm relies on Remote Direct Memory Access (RDMA) for low-latency transfer of states between computing elements, and on state reconstruction trees for compact representation of states on the computing elements themselves. For the distribution of states between computing elements, we propose a concept of state stealing. We have implemented our proposed algorithm using the OpenSHMEM API for RDMA and experimentally evaluated it on the Grid'500 testbed with a set of benchmark models. The experimental results show that our algorithm scales well with the number of available computing elements, and that our state stealing mechanism generally provides a balanced workload distribution.

Abstract We study semi-algorithms to synthesise the constraints under which a Parametric Timed Automaton satisfies some liveness requirement. The algorithms traverse a possibly infinite parametric zone graph, searching for accepting cycles. We provide new search and pruning algorithms, leading to successful termination for many examples. We demonstrate the success and efficiency of these algorithms on a benchmark. We also illustrate parameter synthesis for the classical Bounded Retransmission Protocol. Finally, we introduce a new notion of completeness in the limit, to investigate if an algorithm enumerates all solutions.

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.

Parametric timed automata (PTA) extend timed automata by allowing parameters in clock constraints. Such a formalism is for instance useful when reasoning about unknown delays in a timed system. Using existing techniques, a user can synthesize the parameter constraints that allow the system to reach a specified goal location, regardless of how much time has passed for the internal clocks. We focus on synthesizing parameters such that not only the goal location is reached, but we also address the following questions: what is the minimal time to reach the goal location? and for which parameter values can we achieve this? We analyse the problem and present a semi-algorithm to solve it. We also discuss and provide solutions for minimizing a specific parameter value to still reach the goal. We empirically study the performance of these algorithms on a benchmark set for PTAs and show that minimal-time reachability synthesis is more efficient to compute than the standard synthesis algorithm for reachability. Data or code related to this paper is available at: [ 26 ].

In this paper we investigate the Timed Alternating-Time Temporal Logic (TATL), a discrete-time extension of ATL. In particular, we propose, systematize, and further study semantic variants of TATL, based on different notions of a strategy. The notions are derived from different assumptions about the agents’ memory and observational capabilities, and range from timed perfect recall to untimed memoryless plans. We also introduce a new semantics based on counting the number of visits to locations during the play. We show that all the semantics, except for the untimed memoryless one, are equivalent when punctuality constraints are not allowed in the formulae. In fact, abilities in all those notions of a strategy collapse to the “counting” semantics with only two actions allowed per location. On the other hand, this simple pattern does not extend to the full TATL. As a consequence, we establish a hierarchy of TATL semantics, based on the expressivity of the underlying strategies, and we show when some of the semantics coincide. In particular, we prove that more compact representations are possible for a reasonable subset of TATL specifications, which should improve the efficiency of model checking and strategy synthesis.

A dynamic partial order reduction (DPOR) algorithm is optimal when it always explores at most one representative per Mazurkiewicz trace. Existing literature suggests that the reduction obtained by the non-optimal, state-of-the-art Source-DPOR (SDPOR) algorithm is comparable to optimal DPOR. We show the first program with $$\mathop {\mathcal {O}} (n)$$ Mazurkiewicz traces where SDPOR explores $$\mathop {\mathcal {O}} (2^n)$$ redundant schedules (as this paper was under review, we were made aware of the recent publication of another paper [3] which contains an independently-discovered example program with the same characteristics). We furthermore identify the cause of this blow-up as an NP-hard problem. Our main contribution is a new approach, called Quasi-Optimal POR, that can arbitrarily approximate an optimal exploration using a provided constant k. We present an implementation of our method in a new tool called Dpu using specialised data structures. Experiments with Dpu, including Debian packages, show that optimality is achieved with low values of k, outperforming state-of-the-art tools.

We propose a distributed implementation of the collapse compression technique used by explicit state model checkers to reduce memory usage. This adapatation makes use of lock-free distributed hash tables based on one-sided communication primitives provided by libraries such as OpenSHMEM. We implemented this technique in the distributed version of the model checker Helena. We report on experiments performed on the Grid'5000 cluster with an implementation over OpenMPI. These reveal that, for some models, this distributed implementation can altogether preserve the memory reduction provided by collapse compression and reduce execution times by allowing the exchanges of compressed states between processes.

This paper studies the analysis and parameter synthesis problems for Parametric Timed Automata (PTA) with properties in Linear-time Temporal Logic (LTL). It introduces a series of variations of Nested Depth-First Search (NDFS). We first study the LTL model checking problem for PTA. Based on a careful analysis of parametric zones, we introduce a new layered NDFS approach to LTL model checking. We integrate this with several techniques to prune the search space. In particular, we apply subsumption abstraction to PTA for the first time. We also propose heuristics on the search order to improve the performance. Next, we study parameter synthesis. To this end, this new layered approach and subsumption are added to a Collecting NDFS scheme. We implemented all algorithms in the Imitator tool and analyse their efficiency in a number of experiments.

Parametric timed automata are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. Parameter synthesis using parametric timed automata is very sensitive to the state space explosion problem. To mitigate this problem, we propose two new exploration orders, i. e., the "ranking strategy" and the "priority based strategy", and compare them with existing strategies. We consider both complete parameter synthesis, and counterexample synthesis where the analysis stops as soon as some parameter valuations are found. Experimental results using IMITATOR show that our new strategies significantly outperform existing approaches, especially in the counterexample synthesis.

CosyVerif aims at gathering within a common framework various existing tools for specification and verification. It has been designed in order to 1) support different formalisms with the ability to easily create new ones, 2) provide a graphical user interface for every formalism, 3) include verification tools called via the graphical interface or via an API as a Web service, and 4) offer the possibility for a developer to integrate his/her own tool without much effort, also allowing it to interact with the other tools. Several tools have already been integrated for the formal verification of (extensions of) Petri nets and timed automata.

Time Petri nets (TPN model) allow the specification of real-time systems involving explicit timing constraints. The main challenge of the analysis of such systems is to construct, with few resources (time and space), a coarse abstraction preserving timed properties. In this paper, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behaviour of bounded TPNs with strong time semantics. The main feature of this abstract representation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves runs and reachable states of the corresponding TPN and allows for verification of both event- and state-based properties.

This special issue is dedicated to selected papers from the 32nd International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, which took place in June 2011 in Newcastle upon Tyne, UK.In a careful reviewing process, 17 regular contributions have been accepted for presentation at the conference among 49 submissions.Then, after the conference, a collection of papers published in the proceedings was selected with the help of the Program Committee members, and the authors were invited to revise and extend their contributions for this special issue.Next, the extended submissions have been examined in another independent reviewing process involving two review rounds to meet the standards of FUNDAMENTA INFORMATICAE.Finally, six contributions have been accepted for publication.The accepted papers give a good overview of some recent developments in the area of Petri nets and other models of concurrency.

This paper shows how two of the most important analysis methods for Petri nets can be performed in a modular way. We illustrate our techniques by means of modular Place/Transitions nets (modular PT-nets) in which the individual modules interact via shared places and shared transitions. For place invariants we show that it is possible to construct invariants of the total modular PT-net from invariants of the individual modules. For state spaces, we show that it is possible to decide behavioural properties of the modular PT-net from state spaces of the individual modules plus a synchronization graph, without unfolding to the ordinary state space. The generalization of our techniques to high-level Petri nets is rather straightforward.

The theory behind the notions of place invariants and place flows for coloured Petri nets has been known since 1980, but the lack of tool support entails that the practical use of these results has been very limited. The aim of this paper is to help bridging the gaps between the theory and tool support related to place flows, and in this way support the practical use of place flows. There are three related problem areas to attack: finding place flows from the structure and inscriptions of CP-nets, showing how the place flows determine place invariants, and finally finding properties of CP-nets from the place invariants. We show how checking that a set of weights determines a place flow can be formulated as a /spl lambda/-expressions rewriting problem, allowing us to use the whole set of techniques developed inside the field of /spl lambda/-calculus. We also show how these techniques can be used to prove properties such as deadlock-freeness.