Volume
OASIcs, Volume 44
2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)
- Part of: Series: Open Access Series in Informatics (OASIcs)
Event
SynCoP 2015, April 11, 2015, London, United KingdomEditors
Publication Details
- published at: 2015-12-03
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-82-8
- DBLP: db/conf/syncop/syncop2015
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 44, SynCoP'15, Complete Volume
Abstract
OASIcs, Volume 44, SynCoP'15, Complete Volume
Cite as
2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{andre_et_al:OASIcs.SynCoP.2015,
title = {{OASIcs, Volume 44, SynCoP'15, Complete Volume}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015},
URN = {urn:nbn:de:0030-drops-56168},
doi = {10.4230/OASIcs.SynCoP.2015},
annote = {Keywords: Software/Program Verification}
}
Document
Front Matter
Frontmatter, Table of Contents, Preface, Workshop Organization
Abstract
Frontmatter, Table of Contents, Preface, Workshop Organization
Cite as
2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. i-xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{andre_et_al:OASIcs.SynCoP.2015.i,
author = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
title = {{Frontmatter, Table of Contents, Preface, Workshop Organization}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {i--xii},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.i},
URN = {urn:nbn:de:0030-drops-56034},
doi = {10.4230/OASIcs.SynCoP.2015.i},
annote = {Keywords: Frontmatter, Table of Contents, Preface, Workshop Organization}
}
Document
Invited Paper
View Abstraction – A Tutorial (Invited Paper)
Abstract
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.
Cite as
Parosh A. Abdulla, Fréderic Haziza, and Lukáš Holík. View Abstraction – A Tutorial (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{abdulla_et_al:OASIcs.SynCoP.2015.1,
author = {Abdulla, Parosh A. and Haziza, Fr\'{e}deric and Hol{\'\i}k, Luk\'{a}\v{s}},
title = {{View Abstraction – A Tutorial}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {1--15},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.1},
URN = {urn:nbn:de:0030-drops-56057},
doi = {10.4230/OASIcs.SynCoP.2015.1},
annote = {Keywords: program verification, model checking, parameterized systems}
}
Document
Invited Paper
Parameter synthesis for probabilistic real-time systems (Invited Paper)
Abstract
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.
Cite as
Marta Kwiatkowska. Parameter synthesis for probabilistic real-time systems (Invited Paper). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, p. 16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{kwiatkowska:OASIcs.SynCoP.2015.16,
author = {Kwiatkowska, Marta},
title = {{Parameter synthesis for probabilistic real-time systems}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {16--16},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.16},
URN = {urn:nbn:de:0030-drops-56062},
doi = {10.4230/OASIcs.SynCoP.2015.16},
annote = {Keywords: Quantitative verification, Timed automata, Parameter synthesis}
}
Document
Consistency for Parametric Interval Markov Chains
Abstract
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.
Cite as
Benoît Delahaye. Consistency for Parametric Interval Markov Chains. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 17-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{delahaye:OASIcs.SynCoP.2015.17,
author = {Delahaye, Beno\^{i}t},
title = {{Consistency for Parametric Interval Markov Chains}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {17--32},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.17},
URN = {urn:nbn:de:0030-drops-56079},
doi = {10.4230/OASIcs.SynCoP.2015.17},
annote = {Keywords: Specification, Parameters, Markov Chains, Consistency}
}
Document
Guaranteed control of switched control systems using model order reduction and state-space bisection
Abstract
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.
Cite as
Adrien Le Coënt, Florian de Vuyst, Christian Rey, Ludovic Chamoin, and Laurent Fribourg. Guaranteed control of switched control systems using model order reduction and state-space bisection. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 32-46, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{lecoent_et_al:OASIcs.SynCoP.2015.33,
author = {Le Co\"{e}nt, Adrien and de Vuyst, Florian and Rey, Christian and Chamoin, Ludovic and Fribourg, Laurent},
title = {{Guaranteed control of switched control systems using model order reduction and state-space bisection}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {32--46},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.33},
URN = {urn:nbn:de:0030-drops-56089},
doi = {10.4230/OASIcs.SynCoP.2015.33},
annote = {Keywords: Model Order Reduction, guaranteed control, stability control, reachability control, error bounding}
}
Document
Game-based Synthesis of Distributed Controllers for Sampled Switched Systems
Abstract
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.
Cite as
Laurent Fribourg, Ulrich Kühne, and Nicolas Markey. Game-based Synthesis of Distributed Controllers for Sampled Switched Systems. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 48-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{fribourg_et_al:OASIcs.SynCoP.2015.48,
author = {Fribourg, Laurent and K\"{u}hne, Ulrich and Markey, Nicolas},
title = {{Game-based Synthesis of Distributed Controllers for Sampled Switched Systems}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {48--62},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.48},
URN = {urn:nbn:de:0030-drops-56091},
doi = {10.4230/OASIcs.SynCoP.2015.48},
annote = {Keywords: Cyber-physical systems, controller synthesis, games, robustness, partial observation}
}
Document
Parameter and Controller Synthesis for Markov Chains with Actions and State Labels
Abstract
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.
Cite as
Bharath Siva Kumar Tati and Markus Siegle. Parameter and Controller Synthesis for Markov Chains with Actions and State Labels. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 63-76, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{tati_et_al:OASIcs.SynCoP.2015.63,
author = {Tati, Bharath Siva Kumar and Siegle, Markus},
title = {{Parameter and Controller Synthesis for Markov Chains with Actions and State Labels}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {63--76},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.63},
URN = {urn:nbn:de:0030-drops-56107},
doi = {10.4230/OASIcs.SynCoP.2015.63},
annote = {Keywords: Markov chains with actions and state labels, Parameter synthesis, Controller synthesis, Probabilistic model checking}
}
Document
Parametric Verification of Weighted Systems
Abstract
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.
Cite as
Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian Trier Ringsmose, Kim Guldstrand Larsen, and Radu Mardare. Parametric Verification of Weighted Systems. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 77-90, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{christoffersen_et_al:OASIcs.SynCoP.2015.77,
author = {Christoffersen, Peter and Hansen, Mikkel and Mariegaard, Anders and Ringsmose, Julian Trier and Larsen, Kim Guldstrand and Mardare, Radu},
title = {{Parametric Verification of Weighted Systems}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {77--90},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.77},
URN = {urn:nbn:de:0030-drops-56115},
doi = {10.4230/OASIcs.SynCoP.2015.77},
annote = {Keywords: parametric weighted transition systems, parametric weighted CTL, parametric model checking, well-quasi ordering, tool}
}
Document
Tuning PI controller in non-linear uncertain closed-loop systems with interval analysis
Abstract
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.
Cite as
Julien Alexandre dit Sandretto, Alexandre Chapoutot, and Olivier Mullier. Tuning PI controller in non-linear uncertain closed-loop systems with interval analysis. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 91-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{alexandreditsandretto_et_al:OASIcs.SynCoP.2015.91,
author = {Alexandre dit Sandretto, Julien and Chapoutot, Alexandre and Mullier, Olivier},
title = {{Tuning PI controller in non-linear uncertain closed-loop systems with interval analysis}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {91--102},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.91},
URN = {urn:nbn:de:0030-drops-56125},
doi = {10.4230/OASIcs.SynCoP.2015.91},
annote = {Keywords: PID Tuning, Guaranteed numerical integration, non-linear ordinary differential equations}
}
Document
Informal Presentation
Discrete Parameters in Petri Nets (Informal Presentation)
Abstract
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.
Cite as
Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Discrete Parameters in Petri Nets (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, p. 103, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{david_et_al:OASIcs.SynCoP.2015.103,
author = {David, Nicolas and Jard, Claude and Lime, Didier and Roux, Olivier H.},
title = {{Discrete Parameters in Petri Nets}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {103--103},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.103},
URN = {urn:nbn:de:0030-drops-56046},
doi = {10.4230/OASIcs.SynCoP.2015.103},
annote = {Keywords: Petri nets, Parameters, Coverability}
}
Document
Informal Presentation
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation)
Abstract
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.
Cite as
Étienne André, Camille Coti, and Hoang Gia Nguyen. Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 104-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{andre_et_al:OASIcs.SynCoP.2015.104,
author = {Andr\'{e}, \'{E}tienne and Coti, Camille and Nguyen, Hoang Gia},
title = {{Enhanced Distributed Behavioral Cartography of Parametric Timed Automata}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {104--105},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.104},
URN = {urn:nbn:de:0030-drops-56134},
doi = {10.4230/OASIcs.SynCoP.2015.104},
annote = {Keywords: Formal methods, model checking, distributed algorithmic, real-time systems, parameter synthesis}
}
Document
Informal Presentation
Parameter Synthesis with IC3 (Informal Presentation)
Abstract
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.
Cite as
Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter Synthesis with IC3 (Informal Presentation). In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 106-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cimatti_et_al:OASIcs.SynCoP.2015.106,
author = {Cimatti, Alessandro and Griggio, Alberto and Mover, Sergio and Tonetta, Stefano},
title = {{Parameter Synthesis with IC3}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {106--107},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {Andr\'{e}, \'{E}tienne and Frehse, Goran},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.106},
URN = {urn:nbn:de:0030-drops-56144},
doi = {10.4230/OASIcs.SynCoP.2015.106},
annote = {Keywords: Parameter Synthesis, Infinite-state Transition Systems, Satisfiability Modulo Theories, IC3}
}