SynCoP 2018

(formerly SynCoP + PV)

5th International Workshop on Synthesis of Complex Parameters

This event is an ETAPS workshop organized as a series of invited talks. 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 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.

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.

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,
  • parameterized 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, etc.


SynCoP general chair (2018)
SynCoP (formerly SynCoP + PV) steering committee

Call for papers

In addition to invited presentations (see below), SynCoP 2018 organizes 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) single column. All accepted abstracts will be maid available to the participants of SynCoP 2018 but they will not result in referenced publications.

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

Submission will be made in English in PDF format through Easychair:

See the call for papers for further details.

  • Deadline: 15th January, 2018 29th January, 2018 12th February, 2018
  • Notification: 22nd January, 2018 5th February, 2018 19th February, 2018
  • Final version: 20th March, 2018


Saturday, 14th of April 2018

Time Speaker Topic
9h-10h Keynote speaker 1: Nathalie Bertrand Population control: how to win when intuition fails? [slides]
10h-10h30 Coffee break
10h30-12h30 Session 1
Invited talk: Thao Dang
Invited talk: Marco Faella

Parameter synthesis for biological systems modelling
Controller synthesis for Linear Hybrid Systems [slides]
12h30-14h Lunch break
14h-15h30 Session 2:
Invited talk: Karin Quaas
Paulin Fournier
Mathias Ramparison

The Precise Complexity of the Reachability Problem for Parametric Timed Automata with a Single Parametric Clock
Parametric timed broadcast protocols
Timed automata with parametric resets
15h30-16h Coffee break
20h Workshop dinner 22 Paleon Patron Germanou

Sunday, 15th of April 2018

Time Speaker Topic
9h-10h Keynote speaker 2: Ichiro Hasuo Approximating Reachability Probabilities by (Super-)Martingales [slides]
10h-10h30 Coffee break
10h30-12h35 Session 4:
Invited talk: Pierre Ganty
Benoît Delahaye

Population protocols and predicates
Statistical Model Checking for Parameterized Model [slides]
12h30-14h Lunch break

Invited speakers

Nathalie Bertrand

Nathalie Bertrand (Rennes, France)

Population control: how to win when intuition fails?

We consider a population of identical NFA, and view it as a 2-player game: the first player chooses which action to play, and the second one resolves the non- determinism in each copy of the NFA. The objective for the first player is to synchronize all copies to a target state. In this talk, we will report on decidability and complexity of the following parameterized control problem: for every population size, does the first player have a winning strategy ?

Thao Dang

Thao Dang (Grenoble, France)

Parameter synthesis for biological systems modelling

In this presentation, we consider the problem of parameter synthesis in view of modelling of biological systems. Models for describing mechanisms and principles of biological processes often involve numerous parameters which are needed to account for imprecision in our knowledge as well as lack of experimental information. We will discuss methods for finding parameters so that a hybrid model satisfies some biological hypothesis expressed using temporal logics, or to make the model fit actual measurements. Some case studies are presented to illustrate the methods.

Marco Faella

Marco Faella (Napoli, Italy)

Controller synthesis for Linear Hybrid Systems

Linear Hybrid Automata generalize Timed Automata by allowing for more general real-time dynamics. When discrete transitions are partitioned into controllable and uncontrollable ones, this model can represent the interaction of a switching controller with a plant, subject to disturbances. We will review the state of the art on controller synthesis for this model and demonstrate our NYCS tool.

Pierre Ganty

Pierre Ganty (IMDEA Software Institute, Spain)

Population protocols and predicates

In populations protocols, identical, anonymous, finite-state processes interact pairwise through rendez-vous synchronization. Angluin et al. (PODC 2004) introduced population protocols as a distributed computation model. In that context, an interesting subclass of protocols are the ones computing predicates. Intuitively, a population protocol computes a predicate Φ(N) as follows: instantiate the protocol with N processes and let them interact until they reach a stable unanimity on value true or false. I will present results relative to three natural questions:

  • does this protocol computes a predicate?
  • does this protocol computes this predicate?
  • what predicate does this protocol compute?

Ichiro Hasuo

Ichiro Hasuo (Tokyo, Japan)

Approximating Reachability Probabilities by (Super-)Martingales

Reachability is a fundamental problem in the analysis of probabilistic systems. It is well-known that reachability probabilities are efficiently computed for finite-state systems by linear programming. However, this LP method does not apply to systems that have infinitely many configurations, such as probabilistic programs and parametric systems. In such a case, we have to rely on a parametric witness (i.e. a function) for over- or under-approximating reachability probabilities. A well-studied class of such witnesses is that of supermartingales. In this talk I will talk about our recent results that refine existing supermartingale-based methods. The technical keys to those results are: choice of a suitable martingale concentration lemma for over-approximation; and a categorical axiomatization of supermartingales by coalgebras and corecursive algebras. The talk is based on my joint work with Natsuki Urabe, Masaki Hara, Bart Jacobs, Toru Takisaka and Yuichiro Oyabu.

Karin Quaas

Karin Quaas (Leipzig, Germay)

The Precise Complexity of the Reachability Problem for Parametric Timed Automata with a Single Parametric Clock

In parametric timed automata (PTA), clocks can be compared with parameters. The value of a parameter is a priori unknown and it is instantiated during a run by a parameter valuation. The reachability problem is to decide, whether for a given PTA and a target state there exists a parameter valuation and a corresponding run to the target state. Alur, Henzinger, and Vardi (1994) proved that the problem is undecidable for the case that the PTA uses at least three clocks. They also gave a decision procedure for PTA with at most one clock; the precise complexity of the problem was left open. Bundala and Ouaknine recently gave a 2NEXPTIME upper bound and a NEXPTIME lower bound for PTA with one clock. In this talk, we prove that the problem is NEXPTIME-complete. The proof uses a correspondence between PTA and parametric counter automata (established by Bundala and Ouaknine) on the one side, and a correspondence between parametric one-counter automata and classical two-way automata on the other side.
This is joint work with Benedikt Bollig and Arnaud Sangnier.

Past editions

SynCoP + PV