Published: 31st March 2014
DOI: 10.4204/EPTCS.145
ISSN: 2075-2180

EPTCS 145

Proceedings 1st International Workshop on
Synthesis of Continuous Parameters
Grenoble, France, 6th April 2014

Edited by: Étienne André and Goran Frehse

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

Preface

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:

Program

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:

Support and Acknowledgement

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

Program Committee

Organizers and Program Chairs

Program Committee


Integer Parameter Synthesis for Timed Automata

Aleksandra Jovanović (Department of Computer Science, University of Oxford, United Kingdom)
Didier Lime (École Centrale de Nantes, IRCCyN UMR CNRS 6597, Nantes, France)
Olivier H. Roux (École Centrale de Nantes, IRCCyN UMR CNRS 6597, Nantes, France)

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.

References

  1. Rajeev Alur, Thomas A. Henzinger & Moshe Y. Vardi (1993): Parametric Real-time Reasoning. In: ACM Symposium on Theory of Computing, pp. 592–601. Available at http://dx.doi.org/10.1145/167088.167242.
  2. Laura Bozzelli & Salvatore La Torre (2009): Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design 35(2), pp. 121–151. Available at http://dx.doi.org/10.1007/s10703-009-0074-0.
  3. Thomas A. Henzinger, Pei-Hsin Ho & Howard Wong-Toi (1997): HyTech: A model checker for hybrid systems. In: Orna Grumberg: Computer Aided Verification, Lecture Notes in Computer Science 1254. Springer Berlin Heidelberg, pp. 460–463. Available at http://dx.doi.org/10.1007/3-540-63166-6_48.
  4. Thomas Hune, Judi Romijn, Marielle Stoelinga & Frits Vaandrager (2002): Linear Parametric Model Checking of Timed Automata. Journal of Logic and Algebraic Programming 52-53, pp. 183–220. Available at http://dx.doi.org/10.1016/S1567-8326(02)00037-1.
  5. Didier Lime, Olivier H. Roux, Charlotte Seidner & Louis-Marie Traonouez (2009): Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In: 15th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), LNCS 5505. Springer, York, UK, pp. 54–57. Available at http://dx.doi.org/10.1007/978-3-642-00768-2_6.

Parameter Synthesis for Signal Temporal Logic

Alexandre Donzé (University of California, Berkeley)

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 [75] 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 [41310].

References

  1. E. Asarin, A. Donzé, O. Maler & D. Nickovic (2011): Parametric Identification of Temporal Properties. In: RV, pp. 147–160, doi:10.1007/978-3-642-29860-8_12.
  2. R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli & M. Weiglhofer (2007): Specify, Compile, Run: Hardware from PSL. Electronic Notes in Theoretical Computer Science 190(4), pp. 3 – 16, doi:10.1016/j.entcs.2007.09.004. Proceedings of the Workshop on Compiler Optimization meets Compiler Verification (COCV 2007).
  3. A. Donzé (2010): Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In: CAV, pp. 167–170, doi:10.1007/978-3-642-14295-6_17.
  4. A. Donzé, E. Fanchon, L. M. Gattepaille, O. Maler & P. Tracqui (2011): Robustness Analysis and Behavior Discrimination in Enzymatic Reaction Networks. PLoS ONE 6(9), doi:10.1371/journal.pone.0024246.
  5. A. Donzé & O. Maler (2010): Robust Satisfaction of Temporal Logic over Real-Valued Signals. In: FORMATS, pp. 92–106, doi:10.1007/978-3-642-14295-6_17.
  6. G. E. Fainekos, A. Girard, H. Kress-Gazit & G. J. Pappas (2009): Temporal logic motion planning for dynamic robots. Automatica 45(2), pp. 343 – 352, doi:10.1016/j.automatica.2008.08.008.
  7. G.E. Fainekos & G.J. Pappas (2009): Robustness of Temporal Logic Specifications for Continuous-Time Signals. Theoretical Computer Science 410(42), doi:10.1016/j.tcs.2009.06.021.
  8. X. Jin, A. Donzé, J. Deshmukh & S. A. Seshia (2013): Mining Requirements from Closed-loop Control Models. In: HSCC'13, doi:10.1145/2461328.2461337.
  9. O. Maler & D. Nickovic (2004): Monitoring Temporal Properties of Continuous Signals. In: FORMATS/FTRTFT, pp. 152–166, doi:10.1007/978-3-540-30206-3_12.
  10. N. Mobilia, A. Donzé, J.-M. Moulis & E. Fanchon (2012): A Model of the Cellular Iron Homeostasis Network Using Semi-Formal Methods for Parameter Space Exploration. In: HSB, doi:10.4204/EPTCS.92.4.
  11. P. Nuzzo, H. Xu, N. Ozay, J.B. Finn, A.L. Sangiovanni-Vincentelli, R.M. Murray, A. Donzé & S.A. Seshia (2013): A Contract-Based Methodology for Aircraft Electric Power System Design. Access, IEEE PP(99), pp. 1–1, doi:10.1109/ACCESS.2013.2295764.
  12. N. Piterman, A. Pnueli & Y. Sa'ar (2006): Synthesis of Reactive(1) Designs. In: E. Allen Emerson & Kedar S. Namjoshi: VMCAI, Lecture Notes in Computer Science 3855. Springer, pp. 364–380, doi:10.1007/11609773_24.
  13. S. Stoma, A. Donzé, F. Bertaux, O. Maler & G. Batt (2013): STL-based Analysis of TRAIL-induced Apoptosis Challenges the Notion of Type I/Type II Cell Line Classification. PLoS Comput Biol 9(5), pp. e1003056, doi:10.1371/journal.pcbi.1003056.