eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
0
0
10.4230/OASIcs.SynCoP.2015
article
OASIcs, Volume 44, SynCoP'15, Complete Volume
André, Étienne
Frehse, Goran
OASIcs, Volume 44, SynCoP'15, Complete Volume
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015/OASIcs.SynCoP.2015.pdf
Software/Program Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
i
xii
10.4230/OASIcs.SynCoP.2015.i
article
Frontmatter, Table of Contents, Preface, Workshop Organization
André, Étienne
Frehse, Goran
Frontmatter, Table of Contents, Preface, Workshop Organization
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.i/OASIcs.SynCoP.2015.i.pdf
Frontmatter
Table of Contents
Preface
Workshop Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
1
15
10.4230/OASIcs.SynCoP.2015.1
article
View Abstraction – A Tutorial (Invited Paper)
Abdulla, Parosh A.
Haziza, Fréderic
Holík, Lukáš
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model
property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical
Burns' mutual exclusion protocol.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.1/OASIcs.SynCoP.2015.1.pdf
program verification
model checking
parameterized systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
16
16
10.4230/OASIcs.SynCoP.2015.16
article
Parameter synthesis for probabilistic real-time systems (Invited Paper)
Kwiatkowska, Marta
The parameter synthesis problem aims to find parameter valuations that guarantee that a given objective is satisfied for a parametric model. Applications range from automated model repair to optimisation. This lecture will focus on models with probability and real-time and give an overview of recent results concerning parameter synthesis from quantitative temporal logic objectives. Existing algorithmic approaches and experimental results will be discussed, and future research challenges outlined.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.16/OASIcs.SynCoP.2015.16.pdf
Quantitative verification
Timed automata
Parameter synthesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
17
32
10.4230/OASIcs.SynCoP.2015.17
article
Consistency for Parametric Interval Markov Chains
Delahaye, Benoît
Interval Markov Chains (IMCs) are the base of a classic probabilistic specification theory by Larsen and Jonsson in 1991. They are also a popular abstraction for probabilistic systems. In this paper we introduce and study an extension of Interval Markov Chains with parametric intervals. In particular, we investigate the consistency problem for such models and propose an efficient solution for the subclass of parametric IMCs with local parameters only. We also show that this problem is still decidable for parametric IMCs with global parameters, although more complex in this case.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.17/OASIcs.SynCoP.2015.17.pdf
Specification
Parameters
Markov Chains
Consistency
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
32
46
10.4230/OASIcs.SynCoP.2015.33
article
Guaranteed control of switched control systems using model order reduction and state-space bisection
Le Coënt, Adrien
de Vuyst, Florian
Rey, Christian
Chamoin, Ludovic
Fribourg, Laurent
This paper considers discrete-time linear systems controlled
by a quantized law, i.e., a piecewise constant time function taking
a finite set of values. We show how to generate the control by,
first, applying model reduction to the original system, then using a "state-space bisection" method for synthesizing a control at the reduced-order level, and finally computing an upper bound to the
deviations between the controlled output trajectories of the reduced-order model and those of the original model. The effectiveness of our approach is illustrated on several examples of the literature.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.33/OASIcs.SynCoP.2015.33.pdf
Model Order Reduction
guaranteed control
stability control
reachability control
error bounding
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
48
62
10.4230/OASIcs.SynCoP.2015.48
article
Game-based Synthesis of Distributed Controllers for Sampled Switched Systems
Fribourg, Laurent
Kühne, Ulrich
Markey, Nicolas
Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In this paper, we consider a centralized-controller synthesis technique based on state-space decomposition, and use a game-based approach to extend it to a distributed framework.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.48/OASIcs.SynCoP.2015.48.pdf
Cyber-physical systems
controller synthesis
games
robustness
partial observation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
63
76
10.4230/OASIcs.SynCoP.2015.63
article
Parameter and Controller Synthesis for Markov Chains with Actions and State Labels
Tati, Bharath Siva Kumar
Siegle, Markus
This paper introduces a novel approach for synthesizing parameters and controllers for Markov Chains with Actions and State Labels (ASMC). Requirements which are to be met by the controlled system are specified as formulas of asCSL, which is a powerful temporal logic for characterizing both state properties and action sequences of a labeled Markov chain. The paper proposes two separate - but related - algorithms for untimed until type and untimed general
asCSL formulas. In the former case, a set of transition rates and a common rate reduction factor are determined. In the latter case, a controller which is to be composed in parallel with the given
ASMC is synthesized. Both algorithms are based on some rather simple heuristics.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.63/OASIcs.SynCoP.2015.63.pdf
Markov chains with actions and state labels
Parameter synthesis
Controller synthesis
Probabilistic model checking
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
77
90
10.4230/OASIcs.SynCoP.2015.77
article
Parametric Verification of Weighted Systems
Christoffersen, Peter
Hansen, Mikkel
Mariegaard, Anders
Ringsmose, Julian Trier
Larsen, Kim Guldstrand
Mardare, Radu
This paper addresses the problem of parametric model checking for weighted transition systems. We consider transition systems labelled with linear equations over a set of parameters and we use them to provide semantics for a parametric version of weighted CTL where the until and next operators are themselves indexed with linear equations. The parameters change the model-checking problem into a problem of computing a linear system of inequalities that characterizes the parameters that guarantee the satisfiability. To address this problem, we use parametric dependency graphs (PDGs) and we propose a global update function that yields an assignment
to each node in a PDG. For an iterative application of the function, we prove that a fixed point assignment to PDG nodes exists and the set of assignments constitutes a well-quasi ordering, thus ensuring that the fixed point assignment can be found after finitely many iterations. To demonstrate the utility of our technique, we have implemented a prototype tool that computes the constraints on parameters for model checking problems.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.77/OASIcs.SynCoP.2015.77.pdf
parametric weighted transition systems
parametric weighted CTL
parametric model checking
well-quasi ordering
tool
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
91
102
10.4230/OASIcs.SynCoP.2015.91
article
Tuning PI controller in non-linear uncertain closed-loop systems with interval analysis
Alexandre dit Sandretto, Julien
Chapoutot, Alexandre
Mullier, Olivier
The tuning of a PI controller is usually done through simulation, except for few classes of problems, e.g., linear systems. With a new approach for validated integration allowing us to simulate
dynamical systems with uncertain parameters, we are able to design guaranteed PI controllers. In practical, we propose a new method to identify the parameters of a PI controller for non-linear plants with bounded uncertain parameters using tools from interval analysis and validated simulation. This work relies on interval computation and guaranteed numerical integration of ordinary differential equations based on Runge-Kutta methods. Our method is applied to the
well-known cruise-control problem, under a simplified linear version and with the aerodynamic force taken into account leading to a non-linear formulation.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.91/OASIcs.SynCoP.2015.91.pdf
PID Tuning
Guaranteed numerical integration
non-linear ordinary differential equations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
103
103
10.4230/OASIcs.SynCoP.2015.103
article
Discrete Parameters in Petri Nets (Informal Presentation)
David, Nicolas
Jard, Claude
Lime, Didier
Roux, Olivier H.
With the aim of significantly increasing the modeling capability of Petri nets, we suggest models that involve parameters to represent the weights of arcs, or the number of tokens in places. We call these Petri nets parameterised nets or PPNs. Indeed, the introduction of parameters in models aims to improve genericity.
It therefore allows the designer to leave unspecified aspects,
such as those related to the modeling of the environment. This increase in modeling power usually results in greater complexity in the analysis and verification of the model. Here, we consider the property of coverability of markings. Two general questions arise: "Is there a parameter value for which the property is satisfied?" and "Does the property hold for all possible values of the parameters?". We first study the decidability of these issues,
which we show to be undecidable in the general case. Therefore, we also define subclasses of parameterised networks, based on restriction of the use of parameters, depending on whether the parameters are used on places, input or output arcs of transitions or combinations of them. Those subclasses have therefore a dual interest. From a modeling point of view, restrict the use of parameters to tokens, outputs or inputs can be seen as respectively processes or synchronisation of a given number of processes. From a theoretical point of view, it is interesting to introduce those subclasses of PPN in a concern of completeness of the study. We study the relations between those subclasses and prove that, for some subclasses, certain problems become decidable, making these subclasses more usable in practice.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.103/OASIcs.SynCoP.2015.103.pdf
Petri nets
Parameters
Coverability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
104
105
10.4230/OASIcs.SynCoP.2015.104
article
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation)
André, Étienne
Coti, Camille
Nguyen, Hoang Gia
Parametric timed automata (PTA) allow the specification and verification of timed systems incompletely specified, or featuring timing constants that may change either in the design phase, or at runtime. The behavioral cartography of PTA (BC) relies on the idea of covering a bounded parameter domain with tiles, i.e., parts of the parameter domain in which the discrete behavior is uniform. This is achieved by iterating the inverse method (IM) on the (yet uncovered) integer parameter valuations ("points") of the bounded parametric domain: given a reference point, IM generalizes the behavior corresponding to this point by synthesizing a constraint containing other (integer and real-valued) points with the same discrete behavior. Then, given a linear time property, it is easy to partition the parametric domain into a subset of "good" tiles and a subset of "bad" ones (which correspond to good and bad behaviors).
Useful applications of BC include the optimization of timing constants, and the measure of the system robustness (values around the reference parameters) w.r.t. the untimed language. In practice, a parameter domain with a large number of integer points will require a long time to compute BC. To alleviate that, our goal is to take advantage of powerful distributed architectures. Distributing BC is theoretically easy, since it is trivial that two executions of IM from two different points can be performed on two different nodes. However, distributing it efficiently is challenging. For example, calling two executions of IM from two contiguous integer points has a large probability to yield the same tile in both cases, resulting in a loss of time for one of the two nodes. Thus, the critical question is how to distribute efficiently the point on which to call IM. In a previous work, a master-worker scheme is proposed, where the master assigns points to each worker process, which is called a point-based distribution scheme. In this point-based distribution scheme, choosing the point distribution approach on the master side is the key point that will decide the algorithm performance. Since the master has no ability to foresee the tiles
on cartography (the "shape" of a cartography is unknown in general), two or more processes can receive close points, that then yield the same result, leading to a loss of efficiency. Besides that, two or more tiles can overlap each other; hence, the question is whether we stop an going process starting from a point that is already covered by another tile. Finally, a very large parameter domain (with many integer points) can cause a bottleneck phenomenon on the master side since many worker processes ask for point, while the master is busy to find uncovered points. From the previous problems, we proposed an enhanced master-worker distributed algorithm, based on a domain decomposition scheme. The main idea is that the master splits the parameter domain into subdomains, and assigns them to the workers. Then workers will work on their own set of points, hence reducing the probability of choosing close points since the workers work as far as possible from each other. Then, when a worker finishes the coverage of its subdomain, it asks the master for a new subdomain: the master splits a slow worker's subdomain into two parts, and sends it to the fast worker. Furthermore, we used a heuristic approach to decide whether to stop a process working on a point that has been covered by a tile of another worker. In all our experiments, our enhanced distributed algorithm outperforms previous algorithms.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.104/OASIcs.SynCoP.2015.104.pdf
Formal methods
model checking
distributed algorithmic
real-time systems
parameter synthesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Open Access Series in Informatics
2190-6807
2015-12-03
44
106
107
10.4230/OASIcs.SynCoP.2015.106
article
Parameter Synthesis with IC3 (Informal Presentation)
Cimatti, Alessandro
Griggio, Alberto
Mover, Sergio
Tonetta, Stefano
Parametric systems arise in many application domains, from real-time systems to software to cyber-physical systems. Parameters are fundamental to model unknown quantities at design time and allow a designer to explore different instantiation of the system (i.e. every parameter valuation induces a different system), during the early development phases.
A key challenge is to automatically synthesize all the parameter valuations for which the system satisfies some properties. In this talk we focus on the parameter synthesis problem for infinite-state transition systems and invariant properties. We describe the synthesis algorithm Param IC3, which is based on IC3, one of the major recent breakthroughs in SAT-based model checking, and lately extended to the SMT case.
The algorithm follows a general approach that first builds the set of "bad" parameter valuations and then obtain the set of "good" valuations by complement. The approach enumerates the counterexamples that violate the property, extracting from each counterexample a region of bad parameter valuations, existentially quantifying the state variables. ParamIC3 follows the same principles, but it overcomes some limitations of the previous
approach by exploiting the IC3 features. First, IC3 may find a set of counterexamples s_o, ..., s_k, where each state in s_i is guaranteed to reach some of the bad states in s_k in k-i steps; this
is exploited to apply the expensive quantifier elimination on shortest, and thus more amenable, counterexamples. Second, the internal structure of IC3 allows our extension to be integrated in a
fully incremental fashion, never restarting the search from scratch to find a new counterexample.
While various approaches already solve the parameter synthesis problem for several kind of systems, like infinite-state transition systems, timed and hybrid automata, the advantages ParamIC3 are that: it synthesizes an optimal region of parameters, it avoids computing the whole set of the reachable states, it is incremental and applies quantifier elimination only to small formulas.
We present the results of an experimental evaluation performed on benchmarks from the timed and hybrid systems domain. We compared the approach with similar SMT-based techniques and with techniques based on the computation of the reachable states. The results show the potential of our approach.
https://drops.dagstuhl.de/storage/01oasics/oasics-vol044_syncop2015/OASIcs.SynCoP.2015.106/OASIcs.SynCoP.2015.106.pdf
Parameter Synthesis
Infinite-state Transition Systems
Satisfiability Modulo Theories
IC3