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.
Topics of SynCoP
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, …
SynCoP general chair (2017)
- Peter Habermehl, Paris, France
SynCoP steering committee
Saturday, 22nd of April 2017
|9h-10h||Keynote speaker 1: David Šafránek||Parameter synthesis in dynamical systems by model checking [slides]|
Minimizing Markov Chains Beyond Bisimilarity [slides]
Compositional parameter synthesis
Parametric verification of concurrent programs over the Total Store Ordering weak memory model [slides]
Polynomial Interrupt Timed Automata [slides]
Parameterised Verification for Multi-Agent Systems
|20h||Workshop dinner||Il Forno Restaurant
S:t Olofsgatan 8, Uppsala
Sunday, 23rd of April 2017
|9h-10h||Keynote speaker 2: Joost-Pieter Katoen||Advancing Parameter Synthesis in Markov Models [slides]|
Liveness of Parameterized Timed Networks [slides]
Analysis of parameterised timed systems using Horn constraints [slides]
Parametrised Model Checking of Multi-token Systems via the Composition Method
WBTS: the new class of WSTS without WQO [slides]
Verification of Timed Security Protocols with Clock Drift [slides]
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:
- 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.
Alain Finkel (Cachan, France)
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 ﬁnite MC and a positive integer k, we are interested in ﬁnding 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.