|
Published: 31st March 2014 DOI: 10.4204/EPTCS.145 ISSN: 2075-2180 |
| Preface | |
| Integer Parameter Synthesis for Timed Automata Aleksandra Jovanović, Didier Lime and Olivier H. Roux | 1 |
| Parameter Synthesis for Signal Temporal Logic Alexandre Donzé | 3 |
| MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable Karin Quaas | 5 |
| Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs Vahid Hashemi, Hassan Hatefi and Jan Krčál | 19 |
| Setting Parameters for Biological Models With ANIMO Stefano Schivo, Jetse Scholma, Marcel Karperien, Janine N. Post, Jaco van de Pol and Rom Langerak | 35 |
| Toward Parametric Timed Interfaces for Real-Time Components Youcheng Sun, Giuseppe Lipari, Étienne André and Laurent Fribourg | 49 |
| Worst-case Throughput Analysis for Parametric Rate and Parametric Actor Execution Time Scenario-Aware Dataflow Graphs Mladen Skelin, Marc Geilen, Francky Catthoor and Sverre Hendseth | 65 |
This volume contains the proceedings of the 1st International Workshop on Synthesis of Continuous Parameters (SynCoP'14). The workshop was held in Grenoble, France on April 6th, 2014, as a satellite event of the 17th European Joint Conferences on Theory and Practice of Software (ETAPS'14).
SynCoP aims at bringing together researchers working on parameter synthesis for systems with continuous variables, where the parameters consist of a (usually dense) set of constant values. Synthesis problems for such parameters arise for real-time, hybrid or probabilistic systems in a large variety application domains. A parameter could be, e.g., a delay in a real-time system, or a reaction rate in a biological cell model. The objective of the synthesis problem is to identify suitable parameters to achieve desired behavior, or to verify the behavior for a given range of parameter values.
The scientific subject of the workshop covers (but is not limited to) the following areas:
This volume contains seven contributions: two invited talks and five regular papers.
The two invited talks are:
The workshop received seven submissions, five of which were accepted. Each regular paper was reviewed by at least three different reviewers. The five regular papers are:
Furthermore, one informal presentation was made at the workshop:
SynCoP 2014 is partially supported by Verimag, LIPN, Université Paris 13, and CNRS GDR IM. We would like to thank these various entities for their generous financial and organizational support, thanks to which the workshop was able to sponsor two invited speakers and two students attending the workshop.
SynCoP has been organized as a satellite event of ETAPS'14. We thank the authors for their contributions, the program committee members for reviewing and selecting the papers, and the ETAPS organizing committee Axel Legay, Ylies Falcone, Saddek Bensalem and Marius Bozga for their support. We would also like to thank Laurent Fribourg, Laure Petrucci, and Gilles Villard. Finally, we would like to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science, and in particular Editor-in-Chief Rob van Glabbeek for his support.
In Villetaneuse and Grenoble,
Étienne André and Goran Frehse
In this talk, we address the problem of parametric verification for real-time systems. The correct design of such systems is certainly an important and challenging issue. Introducing parameters in the verification process has a manifold benefit: it makes it more useful by providing the designer with more information than the mere satisfaction of properties, it also makes it more flexible by allowing verification at an earlier stage of the design process when not so many features are fixed. It may finally make the verification process more robust to small changes in the specification.
The main problem encountered in this setting is that parametric verification for timed systems is very difficult. Starting with the seminal results of Alur, Henzinger and Vardi [1], this field mostly features a long list of undecidable problems, to which we will add some more in this talk.
Subclassing the general model of parametric timed automata (PTA) permits to retrieve some decidability, like for PTA with one parametric clock [1] or L/U automata [4,2]. The latter are tailored to the obtain the decidability of the existence of parameter values that make reachability decidable, but will show that the actual synthesis of those parameters is still mostly out of reach.
To overcome these difficulties, we propose a different approach, in which we consider that the parameters should take bounded integer values. We argue that this is not such a restrictive setting, since the bound can be arbitrarily large and since real-life features like transmission times, watchdog durations, activation periods of tasks are reasonably specified by integers, or at least rationals that can be made integers with adequate scaling.
In this setting most problems are obviously decidable, including actual synthesis, since one need only enumerate all possible parameter values and perform non-parametric verification for all of them. This is however not what we want to do in practice, since it is certain to be very inefficient for large (absolute values of the) bounds on parameters. Instead we propose, a symbolic polyhedra-based computation, in the spirit of the classical symbolic semi-algorithms on hybrid systems [3], and making use of the notion of integer hull. We will also discuss the extent of the underapproximation obtained through these symbolic algorithms. These symbolic algorithms have been implemented in our tool ROMEO [5] and we will provide some benchmarking of the proposed techniques.
Finally, we will show that the actual worst-case complexity of problems in this bounded integer parametric setting is (theoretically) very close to that of the corresponding non-parametric versions, and that lifting either the integer or bounded assumption on parameter values leads to undecidability.
In the domain of model-based design using formal methods and tools, synthesis appears as the Holy Grail.
Given a set of specifications, it supposedly allows to generate automatically the design of a system which is
correct-by-construction with respect to those specifications. In order to become a reality, synthesis requires to be
casted in strict and precise framework. Early investigation have focused on finite state machines and linear
temporal logics (LTL) but remained for a long time a purely theoretical exploration due to a seemingly
unavoidable astronomical complexity of the synthesis algorithm. Nevertheless, a polynomial-time algorithm was
eventually developped for a subset of LTL [12] which opened the way for practical implementations
and applications in various fields: digital circuits[2], robotics [6], supervisory control [11], etc.
Synthesis for more complex systems, in particular hybrid systems involving continuous dynamics together
with discrete components, brings yet additional challenges. For these systems, the use of a specification language
adapted to properties of dense-time real-valued signal , namely Signal Temporal Logic (STL) [9], has been
recently advocated. However, synthesizing a hybrid system from STL specifications is by large still an open
problem. The difficulty of this problem can be mitigated by the introduction of parameterizations, both of the
system to be synthesized and for the input specification. An appropriate parameteriterization of the system
allows to reduce synthesis to the problem of finding a valuation for finite set of parameters for which the
system’s behaviors satisfy the specifications. In the case of STL, recently introduced quantitative semantics
[7, 5] can be leveraged to solve this problem. Indeed, when dealing with continuous dynamics and
numerical quantities, yes/no answers provide only partial information and can be augmented with
quantitative information about the satisfaction to provide a better basis for decision making. The
principle is to map parameters to some (signed) distance from satisfying the specification. Parameter
synthesis can then be reduced to an optimization problem with such distance as a cost function.
Introducing parameters in STL specifications leads to PSTL fomulas [1]. Parameter synthesis for PSTL is
dual to the problem of STL synthesis for a parameterized system. It is especially relevant in case the initial
specification reveals to be infeasible, or more generally if the specification has to be revised after a first synthesis
attempt, which is very frequent in practice in synthesis. It is usually the case indeed that the design process
consists of actual co-design of a system and its specifications rather than a waterfall process from the
specification to the design, even considering that an ideal synthesis tool is available. In [1] and later in [8], the
problem of synthesizing parameter valuations for a PSTL formula and a (set of) execution traces
has been considered. It was shown to be undecidable, however a general optimization problem
formulation leveraging again quantitative semantics can be applied. Moreover, situations where
efficient algorithms apply have been characterized. More specifically, when the parameters to be
instantiated are monotic with respect the satisfaction of the formula, then generalized binary search can
be used to find tight valuations, i.e., satisfying valuations which are close to the boundary with
violation.
The tool Breach [3] provides a versatile framework to perform simulation-based parameter synthesis for PSTL formulas and systems described as ordinary differential equations, Simulink, or a generic blackbox simulation function. It has been applyied in industrial contexts in the automative domain [8] and for the analysis of complex biological systems [4, 13, 10].