2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15), SynCoP 2015, April 11, 2015, London, United Kingdom
SynCoP 2015
April 11, 2015
London, United Kingdom
Open Access Series in Informatics
OASIcs
https://www.dagstuhl.de/dagpub/2190-6807
https://dblp.org/db/series/oasics
2190-6807
Étienne
André
Étienne André
Goran
Frehse
Goran Frehse
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
44
2015
978-3-939897-82-8
https://www.dagstuhl.de/dagpub/978-3-939897-82-8
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter
Table of Contents
Preface
Workshop Organization
i-xii
Front Matter
Étienne
André
Étienne André
Goran
Frehse
Goran Frehse
10.4230/OASIcs.SynCoP.2015.i
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
View Abstraction – A Tutorial (Invited Paper)
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.
program verification
model checking
parameterized systems
1-15
Invited Paper
Parosh A.
Abdulla
Parosh A. Abdulla
Fréderic
Haziza
Fréderic Haziza
Lukáš
Holík
Lukáš Holík
10.4230/OASIcs.SynCoP.2015.1
P. A. Abdulla and G. Delzanno. On the coverability problem for constrained multiset rewriting. In Proc. AVIS'06, 5th Int. Workshop on on Automated Verification of Infinite-State Systems, 2006.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. Counter-example guided fence insertion under tso. In Proc. TACAS '08, 18th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of Lecture Notes in Computer Science, 2012.
Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata. Multi-clock timed networks. In Proc. LICS '04, 20th IEEE Int. Symp. on Logic in Computer Science, pages 345-354, 2004.
Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. All for the price of few (parameterized verification through view abstraction). In VMCAI, volume 7737 of LNCS, pages 476-495, 2013.
Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. An integrated specification and verification technique for highly concurrent data structures. In TACAS, volume 7795 of LNCS, pages 324-338, 2013.
Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Regular model checking without transducers (on efficient verification of parameterized systems). In Proc. TACAS '07, 13th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 4424 of Lecture Notes in Computer Science, pages 721-736. Springer Verlag, 2007.
Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. Handling parameterized systems with non-atomic global conditions. In Proc. VMCAI '08, 9th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, 2008.
Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In LICS, pages 160-170. IEEE Computer Society, 1993.
Parosh Aziz Abdulla, Axel Legay, Julien d'Orso, and Ahmed Rezine. Simulation-based iteration of tree transducers. In Proc. TACAS '05, 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 3440 of Lecture Notes in Computer Science, 2005.
Parosh Aziz Abdulla and Aletta Nylén. Timed Petri nets and BQOs. In Proc. ICATPN'2001: 22nd Int. Conf. on application and theory of Petri nets, volume 2075 of Lecture Notes in Computer Science, pages 53 -70, 2001.
T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck. Parameterized verification with automatically computed inductive assertions. In Berry, Comon, and Finkel, editors, Proc. 13th Int. Conf. on Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, pages 221-234, 2001.
M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. On the verification problem for weak memory models. In POPL, pages 7-18. ACM, 2010.
Bernard Boigelot, Axel Legay, and Pierre Wolper. Iterating transducers in the large. In Proc. 15th Int. Conf. on Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 223-235, 2003.
A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract regular model checking. In Proc. 16th Int. Conf. on Computer Aided Verification, volume 3114 of Lecture Notes in Computer Science, pages 372-386, Boston, July 2004. Springer Verlag.
D. Dams, Y. Lakhnech, and M. Steffen. Iterating transducers. In G. Berry, H. Comon, and A. Finkel, editors, Computer Aided Verification, volume 2102 of Lecture Notes in Computer Science, 2001.
G. Delzanno. Automatic verification of cache coherence protocols. In Emerson and Sistla, editors, Proc. 12th Int. Conf. on Computer Aided Verification, volume 1855 of Lecture Notes in Computer Science, pages 53-68. Springer Verlag, 2000.
Giorgio Delzanno. Verification of consistency protocols via infinite-state symbolic model checking. In FORTE'00, volume 183 of IFIP Conference Proceedings, pages 171-186. Kluwer, 2000.
J. Esparza and S. Schwoon. A bdd-based model checker for recursive programs. In CAV, volume 2102 of LNCS, pages 324-336. Springer, 2001.
Pierre Ganty, Jean-François Raskin, and Laurent Van Begin. A Complete Abstract Interpretation Framework for Coverability Properties of WSTS. In VMCAI'06, volume 3855 of LNCS, pages 49-64. Springer, 2006.
Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check... made efficient. In CAV'05, volume 3576 of LNCS, pages 394-407. Springer, 2005.
Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin. Expand, enlarge and check: New algorithms for the coverability problem of wsts. J. Comput. Syst. Sci., 72(1):180-203, 2006.
S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992.
G. Higman. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. (3), 2(7):326-336, 1952.
Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. Theoretical Computer Science, 256:93-112, 2001.
Kedar S. Namjoshi. Symmetry and completeness in the analysis of parameterized systems. In VMCAI'07, volume 4349 of LNCS, pages 299-313. Springer, 2007.
A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. In Proc. TACAS '01, 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031, pages 82-97, 2001.
A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,infinity)-counter abstraction. In Proc. 14th Int. Conf. on Computer Aided Verification, volume 2404 of Lecture Notes in Computer Science, 2002.
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding power multiprocessors. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 175-186, 2011.
T. Touili. Regular Model Checking using Widening Techniques. Electronic Notes in Theoretical Computer Science, 50(4), 2001. Proc. of VEPAS'01.
N. Yonesaki and T. Katayama. Functional specification of synchronized processes based on modal logic. In IEEE 6th International Conference on Software Engineering, pages 208-217, 1982.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Parameter synthesis for probabilistic real-time systems (Invited Paper)
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.
Quantitative verification
Timed automata
Parameter synthesis
16-16
Invited Paper
Marta
Kwiatkowska
Marta Kwiatkowska
10.4230/OASIcs.SynCoP.2015.16
Milan Ceska, Frits Dannenberg, Marta Z. Kwiatkowska, and Nicola Paoletti. Precise parameter synthesis for stochastic biochemical systems. In Pedro Mendes, Joseph O. Dada, and Kieran Smallbone, editors, Proceedings of the 12th International Conference in Computational Methods in Systems Biology (CMSB 2014), volume 8859 of Lecture Notes in Computer Science, pages 86-98. Springer, 2014.
Marco Diciolla, Chang Hwan Peter Kim, Marta Z. Kwiatkowska, and Alexandru Mereacre. Synthesising optimal timing delays for timed I/O automata. In Tulika Mitra and Jan Reineke, editors, Proceedings of the 14th International Conference on Embedded Software (EMSOFT 2014), pages 16:1-16:10. ACM, 2014.
Aleksandra Jovanović and Marta Z. Kwiatkowska. Parameter synthesis for probabilistic timed automata using stochastic game abstractions. In Joël Ouaknine, Igor Potapov, and James Worrell, editors, Proceedings of the 8th International Workshop on Reachability Problems (RP 2014), volume 8762 of Lecture Notes in Computer Science, pages 176-189. Springer, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Consistency for Parametric Interval Markov Chains
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.
Specification
Parameters
Markov Chains
Consistency
17-32
Regular Paper
Benoît
Delahaye
Benoît Delahaye
10.4230/OASIcs.SynCoP.2015.17
É. André, L. Fribourg, and J. Sproston. An extension of the inverse method to probabilistic timed automata. Formal Methods in System Design, (2):119-145, 2013.
R. Barbuti, F. Levi, P. Milazzo, and G. Scatena. Probabilistic model checking of biological systems with uncertain kinetic rates. Theor. Comput. Sci., 419(0):2 - 16, 2012.
N. Bertrand and P. Fournier. Parameterized verification of many identical probabilistic timed processes. In FSTTCS, volume 24 of LIPIcs, pages 501-513, 2013.
N. Bertrand, P. Fournier, and A. Sangnier. Playing with probabilities in reconfigurable broadcast networks. In FoSSaCS, volume 8412 of LNCS, pages 134-148. Springer, 2014.
F. Biondi, A. Legay, B.F. Nielsen, and A. Wasowski. Maximizing entropy over markov processes. In LATA, volume 7810 of LNCS, pages 128-140. Springer, 2013.
B. Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, and A. Wasowski. Constraint markov chains. Theor. Comput. Sci., 412(34):4373-4404, 2011.
N. Chamseddine, M. Duflot, L. Fribourg, C. Picaronny, and J. Sproston. Computing expected absorption times for parametric determinate probabilistic timed automata. In QEST, pages 254-263. IEEE Computer Society, 2008.
C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In ICTAC, volume 3407 of LNCS, pages 280-294. Springer, 2004.
B. Delahaye, J-P. Katoen, K.G. Larsen, A. Legay, M.L. Pedersen, F. Sher, and A. Wasowski. Abstract probabilistic automata. Inf. Comput., 232:66-116, 2013.
B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, and A. Wasowski. Consistency and refinement for interval markov chains. J. Log. Algebr. Program., 81(3):209-226, 2012.
L.M. Ferrer Fioriti, E.M. Hahn, H. Hermanns, and B. Wachter. Variable probabilistic abstraction refinement. In ATVA, volume 7561 of LNCS, pages 300-316. Springer, 2012.
R. Gori and F. Levi. An analysis for proving probabilistic termination of biological systems. Theor. Comput. Sci., 471(0):27 - 73, 2013.
E.M. Hahn, T. Han, and L. Zhang. Synthesis for PCTL in parametric Markov decision processes. In NSFM, volume 6617 of LNCS, pages 146-161. Springer, 2011.
E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. PARAM: A model checker for parametric Markov models. In CAV, volume 6174 of LNCS, pages 660-664. Springer, 2010.
E.M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. Software Tools for Technology Transfer, 13(1):3-19, 2011.
B. Jonsson and K.G. Larsen. Specification and refinement of probabilistic processes. In LICS, pages 266-277. IEEE Computer, 1991.
R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Decidability results for parametric probabilistic transition systems with an application to security. In SEFM, pages 114-121. IEEE Computer Society, 2004.
R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Parametric probabilistic transition systems for system design and analysis. Formal Aspects of Computing, 19(1):93-109, 2007.
K. Sen, M. Viswanathan, and G. Agha. Model-checking markov chains in the presence of uncertainties. In TACAS, volume 3920 of LNCS, pages 394-410. Springer, 2006.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Guaranteed control of switched control systems using model order reduction and state-space bisection
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.
Model Order Reduction
guaranteed control
stability control
reachability control
error bounding
32-46
Regular Paper
Adrien
Le Coënt
Adrien Le Coënt
Florian
de Vuyst
Florian de Vuyst
Christian
Rey
Christian Rey
Ludovic
Chamoin
Ludovic Chamoin
Laurent
Fribourg
Laurent Fribourg
10.4230/OASIcs.SynCoP.2015.33
M. Althoff, O. Stursberg, and M. Buss. Reachability analysis of linear systems with uncertain parameters and inputs. In Proc. of the 46th IEEE Conference on Decision and Control, pages 726-732, 2007.
A. Antoulas and D. C. Sorensen. Approximation of large-scale dynamical systems: an overview. International Journal of Applied Mathematics and Computer Science, 11(5):1093-1121, 2001.
A. Antoulas, D. C. Sorensen, and S. Gugercin. A survey of model reduction methods for large-scale systems. Contemporary Mathematics, 280:193-219, 2000.
E. Asarin, O. Bournez, D. Thao, O. Maler, and A. Pnueli. Effective synthesis of switching controllers for linear systems. Proc. of the IEEE, 88(7):1011-1025, July 2000.
P. Benner, J.-R. Li, and T. Penzl. Numerical solution of large-scale lyapunov equations, riccati equations, and linear-quadratic optimal control problems. Numerical Linear Algebra with Applications, 15(9):755-777, 2008.
P. Benner and A. Schneider. Balanced truncation model order reduction for lti systems with many inputs or outputs. In Proc. of the 19th International Symposium on Mathematical Theory of Networks and Systems, pages 1971-1974, 2010.
F. Blanchini. Set invariance in control. Automatica, 35(11):1747 - 1767, 1999.
L. Fribourg, U. Kühne, and R. Soulat. Finite controlled invariants for sampled switched systems. Formal Methods in System Design, 45(3):303-329, December 2014.
L. Fribourg and R. Soulat. Control of Switching Systems by Invariance Analysis: Application to Power Electronics. Wiley-ISTE, July 2013. 144 pages.
L. Fribourg and R. Soulat. Stability controllers for sampled switched systems. In Proc. of the 7th Workshop on Reachability Problems in Computational Models (RP), volume 8169 of Lecture Notes in Computer Science, pages 135-145. Springer, September 2013.
B. P. Gibbs. Advanced Kalman Filtering, Least-Squares and Modeling: A Practical Handbook. John Wiley &Sons, 2011.
A. Girard, G. Pola, and P. Tabuada. Approximately bisimilar symbolic models for incrementally stable switched systems. Automatic Control, IEEE Transactions on, 55(1):116-126, Jan 2010.
Antoine Girard. Reachability of uncertain linear systems using zonotopes. In Proc. of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC), volume 3414 of Lecture Notes in Computer Science, pages 291-305. Springer, 2005.
Antoine Girard. Synthesis using approximately bisimilar abstractions: state-feedback controllers for safety specifications. In Proc. of the 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 111-120. ACM, 2010.
A. Han and B.H. Krogh. Reachability analysis of large-scale affine systems using low-dimensional polytopes. In Proc. the 9th International Workshop on Hybrid Systems: Computation and Control (HSCC), volume 3927 of Lecture Notes in Computer Science, pages 287-301. Springer, 2006.
Z. Han and B. H. Krogh. Reachability analysis of hybrid systems using reduced-order models. In American Control Conference, pages 1183-1189. IEEE, 2004.
M. Herceg, M. Kvasnica, C.N. Jones, and M. Morari. Multi-Parametric Toolbox 3.0. In Proc. of the European Control Conference, pages 502-510, Zürich, Switzerland, July 17-19 2013.
M. Mazo Jr., A. Davitian, and P. Tabuada. Pessoa: A tool for embedded controller synthesis. In Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 566-569. Springer, 2010.
B. C. Moore. Principal component analysis in linear systems: Controllability, observability and model reduction. IEEE Transaction on Automatic Control, 26(1), 1981.
S. Mouelhi, A. Girard, and G. Goessler. CoSyMA: a tool for controller synthesis using multi-scale abstractions. In Proc. of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC), pages 83-88. ACM, April 2013.
Octave Web page. http://www.gnu.org/software/octave/.
B. Picasso and A. Bicchi. On the stabilization of linear systems under assigned i/o quantization. IEEE Trans. Automat. Contr., 52(10):1994-2000, 2007.
K. Reif, S. Günther, E. Yaz Sr., and R. Unbehauen. Stochastic stability of the discrete-time extended kalman filter. IEEE Transactions on Automatic Control, 44(4):714-728, 1999.
Paulo Tabuada. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, 2009.
D. Tong, W. Zhou, A. Dai, H. Wang, X. Mou, and Y. Xu. h_∞ model reduction for the distillation column linear system. Circuits Syst Signal Process, 33:3287-3297, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Game-based Synthesis of Distributed Controllers for Sampled Switched Systems
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.
Cyber-physical systems
controller synthesis
games
robustness
partial observation
48-62
Regular Paper
Laurent
Fribourg
Laurent Fribourg
Ulrich
Kühne
Ulrich Kühne
Nicolas
Markey
Nicolas Markey
10.4230/OASIcs.SynCoP.2015.48
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Parameter and Controller Synthesis for Markov Chains with Actions and State Labels
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.
Markov chains with actions and state labels
Parameter synthesis
Controller synthesis
Probabilistic model checking
63-76
Regular Paper
Bharath Siva Kumar
Tati
Bharath Siva Kumar Tati
Markus
Siegle
Markus Siegle
10.4230/OASIcs.SynCoP.2015.63
A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model Checking Continuous Time Markov chains. In Computer-Aided Verfication, 1996.
J. Bachmann, M. Riedl, J. Schuster, and M. Siegle. An efficient symbolic elimination algorithm for the stochastic process algebra tool CASPA. In 35th Int. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM'09), pages 485-496. Springer LNCS 5404, 2009.
C. Baier, L. Cloth, B. Haverkort, M. Kuntz, and M. Siegle. Model checking Markov chains with Actions and State labels. IEEE Trans. on Software Engineering, 33(4):209-224, 2007.
C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. on Software Engineering, 29(7), July 2003.
L. Brim, M. Češka, S. Dražan, and D. Šafránek. Exploring parameter space of stochastic biochemical systems using quantitative model checking. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, volume 8044 of LNCS, pages 107-123. Springer Berlin Heidelberg, 2013.
C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In Theor. Aspects of Computing - ICTAC 2004, volume 3407 of LNCS, pages 280-294. Springer Berlin Heidelberg, 2005.
E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. Param: A model checker for parametric Markov models. In Computer Aided Verification, volume 6174 of LNCS, pages 660-664. Springer Berlin Heidelberg, 2010.
E.M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. Int. Journal on Software Tools for Technology Transfer, 13(1):3-19, 2011.
T. Han, J.-P. Katoen, and A. Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability. In Real-Time Systems Symposium, pages 173-182. IEEE, 2008.
H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Theoretical Computer Science, 274:43-87, 2002.
A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In Proc. 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS' 06), volume 3920 of LNCS, pages 441-444. Springer, 2006.
M. Kuntz and M. Siegle. Deriving symbolic representations from stochastic process algebras. In Process Algebra and Probabilistic Methods, Proc. PAPM-PROBMIV'02, pages 188-206. Springer, LNCS 2399, 2002.
M. Lawford and W.M. Wonham. Supervisory control of probabilistic discrete event systems. In Proc. of the 36th Midwestern Symposium on Circuits and Systems, 1993., pages 327-331, vol.1, 1993.
V. Pantelic, M. Lawford, and S. Postma. A framework for supervisory control of probabilistic discrete event systems. In 12th Int. Workshop on Discrete Event Systems (WODES 2014), pages 477-484, vol.12, 2014.
M. Češka, F. Dannenberg, M. Kwiatkowska, and N. Paoletti. Precise parameter synthesis for stochastic biochemical systems. In Computational Methods in Systems Biology, volume 8859 of LNCS, pages 86-98. Springer International Publishing, 2014.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Parametric Verification of Weighted Systems
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.
parametric weighted transition systems
parametric weighted CTL
parametric model checking
well-quasi ordering
tool
77-90
Regular Paper
Peter
Christoffersen
Peter Christoffersen
Mikkel
Hansen
Mikkel Hansen
Anders
Mariegaard
Anders Mariegaard
Julian Trier
Ringsmose
Julian Trier Ringsmose
Kim Guldstrand
Larsen
Kim Guldstrand Larsen
Radu
Mardare
Radu Mardare
10.4230/OASIcs.SynCoP.2015.77
Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In Logic in Computer Science, 1996. LICS'96. Proceedings., Eleventh Annual IEEE Symposium on, pages 313-321. IEEE, 1996.
Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking in dense real-time. Inf. Comput., 104(1):2-34, 1993.
Rajeev Alur and David L. Dill. Automata for modeling real-time systems. In ICALP, pages 322-335, 1990.
Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, pages 592-601, 1993.
Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. In HSCC, pages 49-62, 2001.
Étienne André, Thomas Chatain, Laurent Fribourg, and Emmanuelle Encrenaz. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 20(05):819-836, 2009.
Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager. Minimum-cost reachability for priced timed automata. In HSCC, pages 147-161, 2001.
Sine Viesmose Birch, Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, and Julian T. Ringsmose. Weighted transition system: From boolean to parametric analysis. 8th semester project at Aalborg University, Department of Computer Science, 2014.
Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite runs in weighted timed automata with energy constraints. In FORMATS 2008. Proceedings, pages 33-47, 2008.
Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, and Julian T. Ringsmose. Parametric verification of weighted systems. Unpublished Technical Report. http://pvtool.dk/tech_draft.pdf.
http://pvtool.dk/tech_draft.pdf
Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, and Julian T. Ringsmose. Prototype tool. URL: http://pvtool.dk/.
http://pvtool.dk/
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample guided abstraction refinement. In Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings, pages 154-169, 2000.
Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35(4):pp. 413-422, 1913.
Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1):63-92, 2001.
Goran Frehse, Sumit Kumar Jha, and Bruce H. Krogh. A counterexample-guided approach to parameter synthesis for linear hybrid automata. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, volume 4981 of Lecture Notes in Computer Science, pages 187-200. Springer Berlin Heidelberg, 2008.
Thomas A. Henzinger and Howard Wong-Toi. Using hytech to synthesize control parameters for a steam boiler. In Jean-Raymond Abrial, Egon Börger, and Hans Langmaack, editors, Formal Methods for Industrial Applications, volume 1165 of Lecture Notes in Computer Science, pages 265-282. Springer Berlin Heidelberg, 1996.
Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952.
Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear parametric model checking of timed automata. J. Log. Algebr. Program., 52-53:183-220, 2002.
Jonas Finnemann Jensen, Kim Guldstrand Larsen, Jiří Srba, and Lars Kaerlund Oestergaard. Local model checking of weighted CTL with upper-bound constraints. In Model Checking Software, pages 178-195. Springer, 2013.
Ron Koymans. Specifying real-time properties with metric temporal logic. Real-Time Systems, 2(4):255-299, 1990.
Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134-152, 1997.
Xinxin Liu and Scott A. Smolka. Simple linear-time algorithms for minimal fixed points. In Automata, Languages and Programming, pages 53-66. Springer, 1998.
Chaiwat Sathawornwichit and Takuya Katayama. A parametric model checking approach for real-time systems design. In Software Engineering Conference, 2005. APSEC'05. 12th Asia-Pacific, pages 8-pp. IEEE, 2005.
Alfred Tarski et al. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics, 5(2):285-309, 1955.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Tuning PI controller in non-linear uncertain closed-loop systems with interval analysis
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.
PID Tuning
Guaranteed numerical integration
non-linear ordinary differential equations
91-102
Regular Paper
Julien
Alexandre dit Sandretto
Julien Alexandre dit Sandretto
Alexandre
Chapoutot
Alexandre Chapoutot
Olivier
Mullier
Olivier Mullier
10.4230/OASIcs.SynCoP.2015.91
K. J. Ãström and T. Hägglund. PID controllers: theory, design, and tuning. Instrument Society of America, Research Triangle Park, NC, 1995.
J. Alexandre dit Sandretto and A. Chapoutot. Validated Solution of Initial Value Problem for Ordinary Differential Equations based on Explicit and Implicit Runge-Kutta Schemes. Research report, ENSTA ParisTech, January 2015.
E. Auer and A. Rauh. Vericomp: a system to compare and assess verified IVP solvers. Computing, 94(2-4):163-172, 2012.
J. Bondia, M. Kieffer, E. Walter, J. Monreal, and J. Picó. Guaranteed tuning of PID controllers for parametric uncertain systems. In Decision and Control, page 2948endash2953. IEEE, 2004.
O. Bouissou, A. Chapoutot, and A. Djoudi. Enclosing temporal evolution of dynamical systems using numerical methods. In NASA Formal Methods, number 7871 in LNCS, pages 108-123. Springer, 2013.
O. Bouissou and M. Martel. GRKLib: a Guaranteed Runge Kutta Library. In Scientific Computing, Computer Arithmetic and Validated Numerics, 2006.
V. Broida. Extrapolation des résponses indicielles apériodiques. Automatisme, XVI, 1969.
J. C. Butcher. Coefficients for the study of Runge-Kutta integration processes. Journal of the Australian Mathematical Society, 3:185-201, 5 1963.
L. H. de Figueiredo and J. Stolfi. Self-Validated Numerical Methods and Applications. Brazilian Mathematics Colloquium monographs. IMPA/CNPq, 1997.
L. Desborough and R. Miller. Increasing customer value of industrial control performance monitoring - Honeywell’s experience. In AIChE Symposium Series, pages 169-189, 2002.
A. Dowling. Modeling and PID controller example - cruise control for an electric vehicle.
E. Hairer, Syvert P. Norsett, and G. Wanner. Solving Ordinary Differential Equations I: Nonstiff Problems. Springer-Verlag, 2nd edition, 2009.
L. Jaulin, M. Kieffer, O. Didrit, and E. Walter. Applied Interval Analysis. Springer, 2001.
Y. Lin and M. A. Stadtherr. Validated solutions of initial value problems for parametric odes. Applied Numerical Mathematics, 57(10):1145-1162, 2007.
R. J. Lohner. Enclosing the solutions of ordinary initial and boundary value problems. Computer Arithmetic, pages 255-286, 1987.
R. Moore. Interval Analysis. Prentice Hall, 1966.
N. Nedialkov, K. Jackson, and G. Corliss. Validated solutions of initial value problems for ordinary differential equations. Appl. Math. and Comp., 105(1):21 - 68, 1999.
A. Neumaier. The wrapping effect, ellipsoid arithmetic, stability and confidence regions. Computing Supplementum, 9, 1993.
J. Vehì, I. Ferrer, and M. À. Sainz. A survey of applications of interval analysis to robust control. In IFAC World Congress, 2002.
J.G. Ziegler and N.B. Nichols. Optimum settings for automatic controllers. Journal of dynamic systems, measurement, and control, 115(2B):220-222, 1993.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Discrete Parameters in Petri Nets (Informal Presentation)
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.
Petri nets
Parameters
Coverability
103-103
Informal Presentation
Nicolas
David
Nicolas David
Claude
Jard
Claude Jard
Didier
Lime
Didier Lime
Olivier H.
Roux
Olivier H. Roux
10.4230/OASIcs.SynCoP.2015.103
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Enhanced Distributed Behavioral Cartography of Parametric Timed Automata (Informal Presentation)
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.
Formal methods
model checking
distributed algorithmic
real-time systems
parameter synthesis
104-105
Informal Presentation
Étienne
André
Étienne André
Camille
Coti
Camille Coti
Hoang Gia
Nguyen
Hoang Gia Nguyen
10.4230/OASIcs.SynCoP.2015.104
Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In STOC, pages 592-601. ACM, 1993.
Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 20(5):819-836, 2009.
Étienne André, Camille Coti, and Sami Evangelista. Distributed behavioral cartography of timed automata. In EuroMPI/ASIA, pages 109-114. ACM, 2014.
Étienne André and Laurent Fribourg. Behavioral cartography of timed automata. In RP, volume 6227 of Lecture Notes in Computer Science, pages 76-90. Springer, 2010.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Parameter Synthesis with IC3 (Informal Presentation)
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.
Parameter Synthesis
Infinite-state Transition Systems
Satisfiability Modulo Theories
IC3
106-107
Informal Presentation
Alessandro
Cimatti
Alessandro Cimatti
Alberto
Griggio
Alberto Griggio
Sergio
Mover
Sergio Mover
Stefano
Tonetta
Stefano Tonetta
10.4230/OASIcs.SynCoP.2015.106
Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter synthesis with IC3. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 165-168, 2013.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode