#### Benjamin Aminof (Vienna, Austria)

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

TBA

22-23 April 2017

Blåsenhus, Uppsala, Sweden

4th International Workshop on Synthesis of Complex Parameters

+

3rd International Workshop on Parameterized Verification

This event is a joint ETAPS workshop organized as a series of invited talks. Everyone is welcome to attend and participate in the discussions (register here).

SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behavior of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g., timing, probabilities, costs) or discrete (e.g., number of processes). The goal can be to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values.

The scientific subject of the workshop covers (but is not limited to) the following areas:

- parameter synthesis,
- parametric model checking,
- regular model checking,
- robustness analysis,
- parametric logics, decidability and complexity issues,
- formalisms such as parametric timed and hybrid automata, parametric time(d) Petri nets, parametric probabilistic (timed) automata, parametric Markov Decision Processes, networks of identical processes,
- interactions between discrete and continuous parameters,
- tools and applications to major areas of computer science, biology and control engineering.

Systems composed of a finite but possibly arbitrary number of identical components occur everywhere from hardware design (e.g. cache coherence protocols) to distributed applications (e.g. client-server applications). Parameterized verification is the task of verifying the correctness of this kind of systems regardless the number of their components. The workshop is aimed at bringing together researchers working on Parameterized Verification using

- Specifications in automata and logic, term and graph rewriting, Petri nets, process algebra, …
- Validation methods via assertional and regular model checking, reachability and coverability decision procedures, abstractions, theorem proving, constraint solving, …
- Applications to hardware design, cache coherence protocols, security and communication protocols, multithreaded and concurrent programs, programs with relaxed memory models, mobile and distributed systems, database languages and systems, biological systems, …

- Peter Habermehl, Paris, France

- Parosh Abdulla, Uppsala, Sweden
- Étienne André, Villetaneuse, France
- Kim Larsen, Aalborg, Denmark
- Didier Lime, Nantes, France
- Wojciech Penczek, Warszawa, Poland
- Laure Petrucci, Villetaneuse, France

- Parosh Abdulla, Uppsala, Sweden
- Giorgio Delzanno, Genoa, Italy

Time | Speaker | Topic |
---|---|---|

9h-10h | Keynote speaker 1: David Safranek | Parameter synthesis in dynamical systems by model checking |

10h-10h30 | Coffee break | |

10h30-12h30 | Session 1
Kim Larsen Saddek Bensalem |
TBA Compositional parameter synthesis |

12h30-14h | Lunch break | |

14h-15h30 | Session 2:
Ahmed Bouajjani Béatrice Bérard |
Parametric verification of concurrent programs over the Total Store Ordering weak memory model Polynomial Interrupt Timed Automata |

15h30-16h | Coffee break | |

16h-17h30 | Session 3:
Panagiotis Kouvaros Ahmed Rezine |
Parameterised Verification for Multi-Agent Systems TBA |

Time | Speaker | Topic |
---|---|---|

9h-10h | Keynote speaker 2: Joost-Pieter Katoen | Advancing Parameter Synthesis in Markov Models |

10h-10h30 | Coffee break | |

10h30-12h30 | Session 4:
Florian Zuleger Philipp Rümmer Benjamin Aminof |
Liveness of Parameterized Timed Networks Analysis of parameterised timed systems using Horn constraints Parametrised Model Checking of Multi-token Systems via the Composition Method |

12h30-14h | Lunch break | |

14h-15h30 | Session 5:
Alain Finkel Sun Jun |
WBTS: the new class of WSTS without WQO Verification of Timed Security Protocols with Clock Drift |

15h30-16h | Coffee break | |

16h-17h30 | Session 6: probably none |

TBA

We address the problem of parameter synthesis for parametric timed systems (PTS). The motivation comes from industrial configuration problems for production lines. Our method consists in compositionally generating over-approximations for the individual components of the input systems, which are translated, together with global properties, to ∃∀SMT problems. Our translation forms the basis for optimised and robust parameter synthesis for slightly richer models than PTS.

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.

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:

- On the verification problem for weak memory models, by M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. In POPL 2010.
- 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.

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.*

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.

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.

TBA

TBA

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

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.

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.

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.

- SynCoP 2016, Eindhoven, The Netherlands
- SynCoP 2015, London, UK
- SynCoP 2014, Grenoble, France

SynCoP + PV 2017 is a satellite event of ETAPS 2017, that takes place in Uppsala, Sweden.

The workshops take place in the brand new Campus Blåsenhus, not far from Uppsala City Center.

For more information, see the ETAPS 2017 Web site: