SynCoP + PV

Benjamin Aminof (Vienna, Austria)

Parametrised Model Checking of Multi-token Systems via the Composition Method

Béatrice Bérard (Paris, France)

Polynomial Interrupt Timed Automata

Interrupt Timed Automata (ITA) form a subclass of stopwatch automata where reachability and some variants of timed model checking are decidable even in presence of parameters. They are well suited to model and analyze real-time operating systems. We extend ITA with polynomial guards and updates, leading to the class of polynomial ITA (PolITA). We prove that reachability is decidable in 2EXPTIME on PolITA, using an adaptation of the cylindrical algebraic decomposition algorithm for the first-order theory of reals. We also obtain decidability for the model checking of a timed version of CTL and for reachability in several extensions of PolITA. In particular, compared to previous approaches, our procedure handles parameters and clocks in a unified way. We also study expressiveness questions for PolITA and show that PolITA are incomparable with stopwatch automata.

Ahmed Bouajjani (Paris, France)

Parametric verification of concurrent programs over the Total Store Ordering weak memory model

We address the verification of safety properties of shared memory concurrent programs running over TSO. In this model, writes to a shared memory can be delayed and be not visible immediately to other threads, and reads can overtake pending writes issued by the same process. This can be modelled as the effect of using store buffers. We consider first this safety verification problem assuming that store buffers can be of an arbitrary size, and then we address the problem where in addition the number of threads can also be arbitrarily large. This is indeed motivated by the fact that programs should be robust against changes in the parameters of the underlying infrastructure such as the size of buffers or the number of processors. For that, we introduce a dual (yet equivalent) semantics for TSO where load buffers are used instead of store buffers, and where the flow of information is from the memory to load buffers. We show that this new semantics leads to a simple and efficient decision procedure for the considered safety verification problem.

This talk is based on two articles:

1. On the verification problem for weak memory models, by M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. In POPL 2010.
2. The Benefits of Duality in Verifying Concurrent Programs under TSO, by P. A. Abdulla, M. F. Atig, A. Bouajjani, and T. P. Ngo. In CONCUR 2016.

Alain Finkel (Cachan, France)

WBTS: the new class of WSTS without WQO

We present the ideal framework [FG09a,BFM14] which was recently used to obtain new deep results on Petri nets and extensions. If time, we will present the proof of the famous but unknown Erdös-Tarski theorem. We argue that the theory of ideals prompts a renewal of the theory of WSTS by providing a way to define a new class of monotonic systems, the so-called Well Behaved Transition Systems, which properly contains WSTS, and for which coverability is still decidable by a forward algorithm.

This presents the paper Well Behaved Transition Systems, by Michael Blondin, Alain Finkel and Pierre McKenzie.

Joost-Pieter Katoen (Aachen, Germany)

Advancing Parameter Synthesis in Markov Models

A major practical obstacle is that probabilistic model checking assumes that all probabilities (rates) in Markov models are known a priori. However, at early development stages, certain system quantities such as fault rates, reaction rates, packet loss ratios, etc. are often not — or at the best partially — known. In such cases, parametric models can be used, where transition probabilities are specified as arithmetic expressions over real-valued parameters.

This talk considers the problem of parameter synthesis is: Given a finite-state parametric Markov model, what are the parameter values for which a given (conditional) reachability property exceeds a given threshold? Put differently, what probabilities in the system are tolerable such that the overall probability to reach some critical states is below a given threshold like 10^-8? We present an exact approach using SMT techniques, an approximate technique using parameter lifting, and briefly mention a new approach using geometric programming.

Panagiotis Kouvaros (London, England)

Parameterised Verification for Multi-Agent Systems

Interpreted systems is the main formalism to model multi-agent systems; they provide a natural setup to interpret specifications in a variety of agent-based languages including temporal-epistemic logic. In this talk I will introduce parameterised interleaved interpreted systems, an extension of interpreted systems to describe multi-agent systems of arbitrarily many agents. On this formal setting I will present cutoff-based methodologies for their parameterised verification. I will then extend these to alleviate the common limitation to model agents as finite-state structures, and discuss a technique to verify their fault-tolerance. Finally I will discuss an application to the emergence identification problem of robotic swarms and experimental results obtained on MCMAS-P, a tool realising these techniques.

Kim G. Larsen (Aalborg, Denmark)

Minimizing Markov Chains Beyond Bisimilarity

We address the behavioral metric-based approximate minimization problem of Markov Chains (MCs), i.e., given a finite MC and a positive integer k, we are interested in finding a k-state MC of minimal distance to the original. By considering as metric the bisimilarity distance of Desharnais at al., we show that optimal approximations always exist; show that the problem can be solved as a bilinear program; and prove that its threshold problem is in PSPACE and NP-hard. Finally, we present an approach inspired by expectation maximization techniques that provides suboptimal solutions. Experiments suggest that our method gives a practical approach that outperforms the bilinear program implementation run on state-of-the-art bilinear solvers.

Philipp Rümmer (Uppsala, Sweden)

Analysis of parameterised timed systems using Horn constraints

Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular Uppaal timed automata), exhibit limited scalability for systems with large discrete state space, or cannot handle parametrised systems. We explore the use of Horn constraints and off-the-shelf model checkers for analysis of networks of timed automata. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, and can be extended to include various language features, for instance Uppaal-style communication/broadcast channels and BIP-style interactions, and systems with infinite parallelism. Experiments demonstrate the feasibility of the method.

Joint work with Hossein Hojjat, Pavle Subotic, Wang Yi

David Šafránek (Brno, Czech Republic)

Parameter synthesis in dynamical systems by model checking

We will present a method for parameter synthesis in parametrised dynamical systems from CTL specifications. The method works with a dynamical system represented in terms of a finite-state transition system with parametrised transition relation. Technically, the method is based on model checking algorithms adapted to such kind of transition systems. Depending on a particular class of systems, the underlying algorithms can gain advantages from efficient symbolic representations of sets of parameter valuations. We will show several examples of such systems and respective representations. To demonstrate the method, we will describe applications to models representing dynamics of biological systems with complex non-linear behaviour. Additionally, we will discuss an extension of the parameter synthesis method that allows to address the problem of bifurcation analysis (dramatic changes of systems behaviour with respect to small changes in parameter values). To this end, we introduce a specialised version of hybrid CTL. This allows us to describe various behaviour patterns that make a fundamental basis for formalisation of specific problems of bifurcation analysis.

Sun Jun (Singapore)

Parameterized Verification of Timed Security Protocols with Clock Drift

Time is frequently used in security protocols to provide better security. For instance, critical credentials often have limited lifetime which improves the security against brute-force attacks. However, it is challenging to correctly use time in protocol design. In this work, we develop a systematic method to formally specify as well as automatically verify timed security protocols. We first apply timed applied π-calculus as a formal specification language for timed protocols. Then, we define its formal semantics based on timed logic rules, which facilitates efficient verification against various security properties. Timing constants in the protocol and clock drift are encoded as parameters in the rules. The verification result shows the constraints on the parameters which must be satisfied for the security of the protocol. We evaluate our method with multiple timed security protocols. We find a time related security threat in the TESLA protocol, a complex time-related broadcast protocol for lossy channels, when the clocks used by different protocol participants do not share the same clock rate.

Florian Zuleger (Vienna, Austria)

Liveness of Parameterized Timed Networks

We consider the model checking problem of infinite state systems given in the form of parameterized discrete timed networks with multiple clocks. We show that this problem is decidable with respect to specifications given by B- or S-automata. Such specifications are very expressive (they strictly subsume omega-regular specifications), and easily express complex liveness and safety properties. Our results are obtained by modeling the passage of time using symmetric broadcast, and by solving the model checking problem of parameterized systems of untimed processes communicating using k-wise rendezvous and symmetric broadcast. Our decidability proof makes use of automata theory, rational linear programming, and geometric reasoning for solving certain reachability questions in vector addition systems; we believe these proof techniques will be useful in solving related problems.