SynCoP 2019

This event is an ETAPS workshop organised as a series of invited talks and submitted contributions. Everyone is welcome to attend and participate in the discussions. There are no formal proceedings.

Scientific objective of SynCoP

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 behaviour 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 behaviour, or to verify the behaviour for a given range of parameter values.

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). Parameterised verification is the task of verifying the correctness of this kind of systems regardless the number of their components.

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,
• parameterised 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,
• 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, …
• interactions between discrete and continuous parameters,
• tools and 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, …

Committees

Call for papers

In addition to invited presentations, SynCoP 2019 organises a call for papers.

SynCoP seeks short abstracts only.
Recently published works, ongoing works, or works under submission are welcome.

The page limit is 3 pages (excluding bibliography), LNCS style. All accepted abstracts will be made available to the participants of SynCoP 2019 but they will not result in referenced publications.

Authors of accepted abstracts will be required to give a presentation during the workshop.

We intend to select the best abstracts and presentations for a full paper in a special issue of a journal.

Submissions must be made in English in PDF format through Easychair

See the call for papers for further details.

• Deadline: 15 February 2019
• Notification: 22 February 2019
• Final version: 15 March 2019

Invited speakers

The following speakers confirmed their participation:

• Christel Baier (Dresden, Germany): Parametric Markov chains: algorithms, complexity and applications
• Nikola Beneš (Brno, Czech Republic): Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties
• Benoît Delahaye (Nantes, France): Parametric statistical model checking of UAV flightplan
• Peter Habermehl (Paris, France): On Parameterised Jobshop Scheduling Problems
• Nils Jansen (Nijmegen, The Netherlands): Convex Optimization meets Parameter Synthesis for MDPs
• Jan Křetínský (Munich, Germany): Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints
• Laura Nenzi (Trieste, Italy): Parametric Verification and Synthesis based on Gaussian Processes
• Wojciech Penczek (Warsaw, Poland): SMT-based bounded model checking for parametric reaction systems

Program

Invited speakers

Christel Baier (Dresden, Germany)

Parametric Markov chains: algorithms, complexity and applications

Parametric Markov chains have been introduced as model for families of stochastic systems with the same topological structure, but that may differ in the transition probabilities. The talk provides an overview of techniques for computing rational functions as closed-form expressions for reachability probabilities or expected costs and complexity-theoretic results for checking the existence of a parameter valuation such that the induced Markov chains satisfies a PCTL formula. The last part of the talk provides insights in application scenarios of the parametric approach.

Nikola Beneš (Brno, Czech Republic)

Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties

The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. We introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for Clock-Aware LTL properties. Clock-Aware LTL is an extension of LTL that allows to reason about the clock values in the atomic propositions. We propose a symbolic zone-based method for the problem which can be significantly faster than the naive parameter scan solution. Our technique adapts the ideas of the automata-based approach to Clock-Aware LTL model checking of timed automata.

Benoît Delahaye (Nantes, France)

Parametric statistical model checking of UAV flightplan

Unmanned Aerial Vehicles (UAV) are now widespread in our society and are often used in a context where they can put people at risk. Studying their reliability, in particular in the context of flight above a crowd, thus becomes a necessity. In this paper, we study the modeling and analysis of UAV in the context of their flight plan. To this purpose, we build a parametric probabilistic model of the UAV and use it as well as a given flight plan in order to model its trajectory. This model takes into account parameters such as potential filter or sensor (like GPS) failure as well as wind force and direction. Because of the nature and complexity of the obtained models, their exact verification using tools such as PRISM or PARAM is impossible. We therefore develop a new approximation technique, called Parametric Statistical Model Checking, in order to compute failure probabilities. This method has been implemented in a prototype tool, which we use to resolve the problem described above.
This is joint work with Ran Bao and Christian Attiogbe.

Peter Habermehl (Paris, France)

On Parameterised Jobshop Scheduling Problems

In this talk, we consider parameterised versions of the jobshop scheduling problem where a parameterised number of jobs have to complete a sequence of actions some of which are mutually exclusive. The cost of completing the jobs is the total time the jobs spend. We show that in the some cases the parameterised cost function is semilinear and can be computed by using Petri Net techniques.

Nils Jansen (Nijmegen, The Netherlands)

Convex Optimization meets Parameter Synthesis for MDPs

Verification and synthesis problems of parametric Markov decision processes can be naturally expressed as nonlinear programs. Our results are based on two key insights. First, we first observe that many of these computationally demanding problems belong to the subclass of signomial programs. Second, we show how the nonlinear program can be formulated as a quadratically-constrained quadratic program (QCQP) and is non-convex in general. The first insight allows for a sequential optimization algorithm to efficiently compute sound but possibly suboptimal solutions. Each stage of this algorithm solves a convexified version of the original problem. The second insight allows to exploit a convex-concave procedure (CCP) to iteratively obtain local optima. An appropriate interplay between convex optimization solvers and probabilistic model checkers creates a procedure --- realized in the tool PROPheSY --- that is the first to solve the synthesis problem for well-known benchmarks with thousands of parameters. Moreover, employing these scalability improvements, we establish and demonstrate the applicability of parameter synthesis to strategy computation for partially observable Markov decision processes.

Jan Křetínský (Munich, Germany)

Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints

We consider Markov decision processes (MDP) with unknown probabilistic transition function and unknown reward function. We formalize the problem of maximizing the mean-payoff value with high probability while satisfying a parity objective in this setting. This problem can be viewed as strategy synthesis for parametric MDP where the parameters are fixed but unknown. Assuming the support of the unknown transition function and a lower bound on the minimal transition probability are known in advance, we construct probably approximately correct (PAC) strategies w.r.t. the mean payoff objective that guarantee sure or almost-sure satisfaction of a parity condition, depending on the memory allowed. This is a joint work with Guillermo Perez and Jean-Francois Raskin published at Concur'18 and ongoing work.

Laura Nenzi (Trieste, Italy)

Parametric Verification and Synthesis based on Gaussian Processes

Parameter verification and synthesis problems for stochastic systems are still hard challenges. The tasks become even more prohibitive when the systems are large-scale and the verification/synthesis are respect the satisfaction of some linear temporal logic formulae. In this paper, we review a number of techniques that we designed to tackle such problems.
This is joint work with Luca Bortolussi and Simone Silvetti.

Wojciech Penczek (Warsaw, Poland)

SMT-based bounded model checking for parametric reaction systems

Reaction systems are a formal model for specifying and analysing computational processes in which reactions operate on sets of entities (molecules), providing a framework for dealing with qualitative aspects of biochemical systems. This paper is concerned with reaction systems in which entities can have discrete concentrations and reactions operate on multisets of entities, providing a succinct framework for dealing with quantitative aspects of systems. This is facilitated by a dedicated linear time temporal logic which allows one to express and verify a wide range of behavioural system properties. In practical applications, a reaction system with discrete concentrations may only be partially specified, and effective calculation of the missing details would provide an attractive design approach. To develop such an approach, this paper introduces reaction systems with parameters representing the unknown parts of the reactions. The main result is a method which attempts to replace these parameters in such a way that the resulting reaction system operating in a given external environment satisfies a given temporal logic formula. We provide a suitable encoding of parametric reaction systems in SMT, and outline a synthesis procedure based on bounded model checking for solving the synthesis problem. We also provide a complexity result of the synthesis problem and preliminary experimental results demonstrating the feasibility of the new synthesis method.
This is joint work with Artur Męski.

Past editions

SynCoP

• SynCoP 2018, Thessaloniki, Greece
• SynCoP + PV 2017, Uppsala, Sweden
• SynCoP 2016, Eindhoven, The Netherlands
• SynCoP 2015, London, UK
• SynCoP 2014, Grenoble, France

PV

• PV 2015, Madrid, Spain
• PV 2014, Roma, Italy

Contacts

• Laure Petrucci
• Jaco van de Pol

Support