User menu

Accès à distance ? S'identifier sur le proxy UCLouvain

Compositionality for quantitative specifications

Primary tabs

download
  • Open access
  • PDF
  • 742.48 K
Fahrenberg, Uli Křetínský, Jan Legay, Axel [UCL] Traonouez, Louis-Marie

We provide a framework for compositional and iterative design and verification of systems with quantitative information, such as rewards, time or energy. It is based on disjunctive modal transition systems where we allow actions to bear various types of quantitative information. Throughout the design process the actions can be further refined and the information made more precise. We show how to compute the results of standard operations on the systems, including the quotient (residual), which has not been previously considered for quantitative non-deterministic systems. Our quantitative framework has close connections to the modal nu-calculus and is compositional with respect to general notions of distances between systems and the standard operations.

Document type Article de périodique (Journal article) – Article de recherche
Access type Accès libre
Publication date 2017
Language Anglais
Journal information "Soft Computing" - Vol. 22, no.4, p. 1139-1158 (2017)
Peer reviewed yes
Publisher Springer Nature
issn 1432-7643
e-issn 1433-7479
Publication status Publié
Affiliations UCL - SST/ICTM - Institute of Information and Communication Technologies, Electronics and Applied Mathematics
UCL - SST/ICTM/INGI - Pôle en ingénierie informatique
Links
  1. Aceto Luca, Ingolfsdottir Anna, Larsen Kim Guldstrand, Srba Jiri, Reactive Systems : Modelling, Specification and Verification, ISBN:9780511814105, 10.1017/cbo9780511814105
  2. Aceto Luca, Fábregas Ignacio, de Frutos-Escrig David, Ingólfsdóttir Anna, Palomino Miguel, On the specification of modal systems: A comparison of three frameworks, 10.1016/j.scico.2013.02.004
  3. Aliprantis CD, Border KC (2007) Infinite dimensional analysis: a hitchhiker’s guide. Springer, Berlin
  4. Bauer SS, Fahrenberg U, Juhl L, Larsen KG, Legay A, Thrane C (2011) Quantitative refinement for weighted modal transition systems. In: Murlak F, Sankowski P (eds) MFCS, volume 6907 of Lecture Notes Computer Science. Springer, Berlin, pp 60–71
  5. Bauer SS, David A, Hennicker R, Larsen KG, Legay A, Nyman U, Wąsowski A (2012a) Moving from specifications to contracts in component-based design. In: de Lara J, Zisman A (eds) FASE, volume 7212 of Lecture Notes in Computer Science. Springer, Berlin, pp 43–58
  6. Bauer Sebastian S., Fahrenberg Uli, Legay Axel, Thrane Claus, General Quantitative Specification Theories with Modalities, Computer Science – Theory and Applications (2012) ISBN:9783642306419 p.18-30, 10.1007/978-3-642-30642-6_3
  7. Bauer SS, Juhl L, Larsen KG, Legay A, Srba J (2012c) Extending modal transition systems with structured labels. Math Struct Comput Sci 22(4):581–617
  8. Bauer Sebastian S., Fahrenberg Uli, Juhl Line, Larsen Kim G., Legay Axel, Thrane Claus, Weighted modal transition systems, 10.1007/s10703-012-0178-9
  9. Ben-David S, Chechik M, Uchitel S (2013) Merging partial behaviour models with different vocabularies. In: D’Argenio PR, Melgratti HC (eds) CONCUR, volume 8052 of Lecture Notes in Computer Science. Springer, Berlin, pp 91–105
  10. Beneš N., Křetínský J., Larsen K.G., Srba J., On determinism in modal transition systems, 10.1016/j.tcs.2009.06.009
  11. Beneš N, Černá I, Křetínský J (2011) Modal transition systems: composition and LTL model checking. In: Bultan T, Hsiung P-A (eds) ATVA, volume 6996 of Lecture Notes in Computer Science. Springer, Berlin, pp 228–242
  12. Beneš N, Delahaye B, Fahrenberg U, Křetínský J, Legay A (2013) Hennessy-Milner logic with greatest fixed points. In: D’Argenio PR, Melgratti HC (eds) CONCUR, volume 8052 of Lecture Notes in Computer Science. Springer, Berlin, pp 76–90
  13. Bertrand Nathalie, Legay Axel, Pinchinat Sophie, Raclet Jean-Baptiste, Modal event-clock specifications for timed component-based design, 10.1016/j.scico.2011.01.007
  14. Boudol Gérard, Larsen Kim G., Graphical versus logical specifications, 10.1016/0304-3975(92)90276-l
  15. Caillaud Benoît, Delahaye Benoît, Larsen Kim G., Legay Axel, Pedersen Mikkel L., Wąsowski Andrzej, Constraint Markov Chains, 10.1016/j.tcs.2011.05.010
  16. Caires Luı́s, Cardelli Luca, A spatial logic for concurrency (part I), 10.1016/s0890-5401(03)00137-8
  17. Cardelli L, Larsen KG, Mardare R (2011) Modular markovian logic. In: Aceto L, Henzinger M, Sgall J (eds) ICALP(2), volume 6756 of Lecture Notes in Computer Science. Springer, Berlin, pp 380–391
  18. Černý Pavol, Henzinger Thomas A., Radhakrishna Arjun, Simulation distances, 10.1016/j.tcs.2011.08.002
  19. Continuity, modulus of. Encyclopedia of Mathematics. http://www.encyclopediaofmath.org/index.php?title=Continuity,_modulus_of&oldid=30705
  20. David Alexandre, Larsen Kim G., Legay Axel, Nyman Ulrik, Traonouez Louis-Marie, Wąsowski Andrzej, Real-time specifications, 10.1007/s10009-013-0286-x
  21. de Alfaro L, Henzinger TA, Stoelinga M (2002) Timed interfaces. In: Sangiovanni-Vincentelli AL, Sifakis J (eds) EMSOFT, volume 2491 of Lecture Notes in Computer Science, vol 2491. Springer, Berlin, pp 108–122
  22. de Alfaro L (2003) Quantitative verification and control via the mu-calculus. In: Amadio RM, Lugiez D (eds) CONCUR, volume 2761 of Lecture Notes in Computer Science. Springer, Berlin, pp 102–126
  23. de Alfaro Luca, Faella Marco, Henzinger Thomas A., Majumdar Rupak, Stoelinga Mariëlle, Model checking discounted temporal properties, 10.1016/j.tcs.2005.07.033
  24. de Alfaro L., Faella M., Stoelinga M., Linear and Branching System Metrics, 10.1109/tse.2008.106
  25. de Alfaro Luca, Henzinger Thomas A., Interface automata, 10.1145/503209.503226
  26. Delahaye Benoît, Larsen Kim G., Legay Axel, Pedersen Mikkel L., Wa¸sowski Andrzej, Consistency and refinement for Interval Markov Chains, 10.1016/j.jlap.2011.10.003
  27. Delahaye Benoît, Fahrenberg Uli, Larsen Kim, Legay Axel, Refinement and Difference for Probabilistic Automata, 10.2168/lmcs-10(3:11)2014
  28. Desharnais Josée, Gupta Vineet, Jagadeesan Radha, Panangaden Prakash, Metrics for labelled Markov processes, 10.1016/j.tcs.2003.09.013
  29. Fahrenberg U, Acher M, Legay A, Wąsowski A (2014a) Sound merging and differencing for class diagrams. In: Gnesi S, Rensink A (eds) FASE, volume 8411 of Lecture Notes in Computer Science. Springer, Berlin, pp 63–78
  30. Fahrenberg Uli, Legay Axel, Traonouez Louis-Marie, Structural Refinement for the Modal nu-Calculus, Theoretical Aspects of Computing – ICTAC 2014 (2014) ISBN:9783319108810 p.169-187, 10.1007/978-3-319-10882-7_11
  31. Fahrenberg U, Křetínský J, Legay A, Traonouez L-M (2014c) Compositionality for quantitative specifications. In: Lanese I, Madelaine E (eds) FACS, volume 8997 of Lecture Notes in Computer Science. Springer, Berlin, pp 306–324
  32. Fahrenberg Uli, Legay Axel, A Robust Specification Theory for Modal Event-Clock Automata, 10.4204/eptcs.87.2
  33. Fahrenberg U, Legay A (2013) Generalized quantitative analysis of metric transition systems. In: Shan C-C (ed) APLAS, voume 8301 of Lecture Notes in Computer Science. Springer, Berlin, pp 192–208
  34. Fahrenberg U, Legay A (2014a) General quantitative specification theories with modal transition systems. Acta Inform 51(5):261–295
  35. Fahrenberg U, Legay A (2014b) The quantitative linear-time-branching-time spectrum. Theor Comput Sci 538:54–69
  36. Fahrenberg U, Legay A, Thrane C (2011) The quantitative linear-time–branching-time spectrum. In: Chakraborty S, Kumar A (eds) FSTTCS, volume 13 of LIPIcs. pp 103–114
  37. Feuillade Guillaume, Pinchinat Sophie, Modal Specifications for the Control Theory of Discrete Event Systems, 10.1007/s10626-006-0008-6
  38. Girard Jean-Yves, Linear logic, 10.1016/0304-3975(87)90045-4
  39. Hennessy M., Acceptance trees, 10.1145/4221.4249
  40. Henzinger TA, Majumdar R, Prabhu VS (2005) Quantifying similarities between timed systems. In: Pettersson P, Yi W (eds) FORMATS, volume 3829 of Lecture Notes in Computer Science. Springer, Berlin, pp 226–241
  41. Henzinger TA, Sifakis J (2006) The embedded systems design challenge. In: Misra J, Nipkow T, Sekerinski E (eds) FM, volume 4085 of Lecture Notes in Computer Science. Springer, Berlin, pp 1–15
  42. Huth M., Kwiatkowska M., Quantitative analysis and model checking, 10.1109/lics.1997.614940
  43. Jacobs B, Poll E (2001) A logic for the Java modeling language JML. In: Hußmann H (ed) FASE, volume 2029 of Lecturte Notes in Computer Science. Springer, Berlin, pp 284–299
  44. Jonsson B., Larsen K.G., Specification and refinement of probabilistic processes, 10.1109/lics.1991.151651
  45. Klin Bartek, Sassone Vladimiro, Structural operational semantics for stochastic and weighted transition systems, 10.1016/j.ic.2013.04.001
  46. Kozen Dexter, Results on the propositional μ-calculus, 10.1016/0304-3975(82)90125-6
  47. Křetínský J, Sickert S (2013) MoTraS: a tool for modal transition systems and their extensions. In: Van Hung D, Ogawa M (eds) ATVA, volume 8172 of Lecture Notes in Computer Science. Springer, Berlin, pp 487–491
  48. Larsen KG, Thomsen B (1998) A modal process logic. In: LICS. IEEE Computer Society, pp 203–210
  49. Larsen K.G., Xinxin L., Equation solving using modal transition systems, 10.1109/lics.1990.113738
  50. Larsen Kim G., Proof systems for satisfiability in Hennessy-Milner Logic with recursion, 10.1016/0304-3975(90)90038-j
  51. Larsen KG, Legay A, Traonouez L-M, Wąsowski A (2011) Robust specification of real time components. In: Fahrenberg U, Tripakis S (eds) FORMATS, volume 6919 of Lecture Notes in Computer Science. Springer, Berlin, pp 129–144
  52. Larsen KG, Mardare R, Panangaden P (2012) Taking it to the limit: approximate reasoning for Markov processes. In: Rovan B, Sassone V, Widmayer P (eds) MFCS, volume 7464 of Lecture Notes in Computer Science. Springer, Berlin, pp 681–692
  53. Larsen Kim G., Legay Axel, Traonouez Louis-Marie, Wąsowski Andrzej, Robust synthesis for real-time systems, 10.1016/j.tcs.2013.08.015
  54. Liskov Barbara H., Wing Jeannette M., A behavioral notion of subtyping, 10.1145/197320.197383
  55. Mio M (2011) Probabilistic modal mu-calculus with independent product. In: Hofmann M (ed) FOSSACS, volume 6604 of Lecture Notes in Computer Science. Springer, Berlin, pp 290–304
  56. Morgan C, McIver A (1997) A probabilistic temporal calculus based on expectations. In: Groves L, Reeves S (eds) Formal methods. Springer, Singapore
  57. Raclet J-B (2007) Residual for component specifications. In: Publication interne 1843. IRISA, Rennes
  58. Romero-Hernández D, de Frutos-Escrig D (2012a) Defining distances for all process semantics. In: Giese H, Rosu G (eds) FMOODS/FORTE, volume 7273 of Lecture Notes in Computer Science. Springer, Berlin, pp 169–185
  59. Romero-Hernández D, de Frutos-Escrig D (2012b) Distances between processes: a pure algebraic approach. In: Martí-Oliet N, Palomino M (eds) WADT, volume 7841 of Lecture Notes in Computer Science. Springer, Berlin, pp 265–282
  60. Sifakis J (2011) A vision for computer science-the system perspective. Cent Eur J Comput Sci 1(1):108–116
  61. Traonouez Louis-Marie, A Parametric Counterexample Refinement Approach for Robust Timed Specifications, 10.4204/eptcs.87.3
  62. Uchitel S, Chechik M (2004) Merging partial behavioural models. In: Taylor RN, Dwyer MB (eds) SIGSOFT FSE. ACM, New York, pp 43–52
  63. van Breugel Franck, Worrell James, A behavioural pseudometric for probabilistic transition systems, 10.1016/j.tcs.2004.09.035
Bibliographic reference Fahrenberg, Uli ; Křetínský, Jan ; Legay, Axel ; Traonouez, Louis-Marie. Compositionality for quantitative specifications. In: Soft Computing, Vol. 22, no.4, p. 1139-1158 (2017)
Permanent URL http://hdl.handle.net/2078.1/217088