×

zbMATH — the first resource for mathematics

Compositionality for quantitative specifications. (English) Zbl 1398.68339
Summary: 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.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Motras; JML; SLMC
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Aceto L, Ingólfsdóttir A, Larsen KG, Srba J (2007) Reactive systems. Cambridge University Press, Cambridge · Zbl 1141.68043
[2] Aceto, L; Fábregas, I; Frutos-Escrig, D; Ingólfsdóttir, A; Palomino, M, On the specification of modal systems: a comparison of three frameworks, Sci Comput Program, 78, 2468-2487, (2013)
[3] Aliprantis CD, Border KC (2007) Infinite dimensional analysis: a hitchhiker’s guide. Springer, Berlin · Zbl 0938.46001
[4] Bauer, SS; Fahrenberg, U; Juhl, L; Larsen, KG; Legay, A; Thrane, C; Murlak, F (ed.); Sankowski, P (ed.), Quantitative refinement for weighted modal transition systems, 60-71, (2011), Berlin · Zbl 1343.68150
[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 SS, Fahrenberg U, Legay A, Thrane C (2012b) General quantitative specification theories with modalities. In: Hirsch EA, Karhumäki J, Lepistö A, Prilutskii M (eds) CSR, volume 7353 of Lecture Notes in Computer Science. Springer, Berlin, pp 18-30 · Zbl 1360.68576
[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 · Zbl 1277.68160
[8] Bauer, SS; Fahrenberg, U; Juhl, L; Larsen, KG; Legay, A; Thrane, C, Weighted modal transition systems, Form Methods Syst Des, 42, 193-220, (2013) · Zbl 1291.68246
[9] Ben-David, S; Chechik, M; Uchitel, S; D’Argenio, PR (ed.); Melgratti, HC (ed.), Merging partial behaviour models with different vocabularies, 91-105, (2013), Berlin · Zbl 1390.68458
[10] Beneš, N; Křetínský, J; Larsen, KG; Srba, J, On determinism in modal transition systems, Theor Comput Sci, 410, 4026-4043, (2009) · Zbl 1186.68314
[11] Beneš, N; Černá, I; Křetínský, J; Bultan, T (ed.); Hsiung, P-A (ed.), Modal transition systems: composition and LTL model checking, 228-242, (2011), Berlin · Zbl 1348.68119
[12] Beneš, N; Delahaye, B; Fahrenberg, U; Křetínský, J; Legay, A; D’Argenio, PR (ed.); Melgratti, HC (ed.), Hennessy-milner logic with greatest fixed points, 76-90, (2013), Berlin · Zbl 1271.68131
[13] Bertrand, N; Legay, A; Pinchinat, S; Raclet, J-B, Modal event-clock specifications for timed component-based design, Sci Comput Program, 77, 1212-1234, (2012) · Zbl 1264.68053
[14] Boudol, G; Larsen, KG, Graphical versus logical specifications, Theor Comput Sci, 106, 3-20, (1992) · Zbl 0776.68084
[15] Caillaud, B; Delahaye, B; Larsen, KG; Legay, A; Pedersen, ML; Wąsowski, A, Constraint Markov chains, Theor Comput Sci, 412, 4373-4404, (2011) · Zbl 1223.68070
[16] Caires, L; Cardelli, L, A spatial logic for concurrency (part I), Inf Comput, 186, 194-235, (2003) · Zbl 1068.03022
[17] Cardelli, L; Larsen, KG; Mardare, R; Aceto, L (ed.); Henzinger, M (ed.); Sgall, J (ed.), Modular Markovian logic, 380-391, (2011), Berlin
[18] Černý, P; Henzinger, TA; Radhakrishna, A, Simulation distances, Theor Comput Sci, 413, 21-35, (2012) · Zbl 1234.68253
[19] Continuity, modulus of. Encyclopedia of Mathematics. http://www.encyclopediaofmath.org/index.php?title=Continuity,_modulus_of&oldid=30705
[20] David, A; Larsen, KG; Legay, A; Nyman, U; Traonouez, L-M; Wąsowski, A, Real-time specifications, Int J Softw Tools Technol Transf, 17, 17-45, (2015)
[21] Alfaro, L; Henzinger, TA; Stoelinga, M; Sangiovanni-Vincentelli, AL (ed.); Sifakis, J (ed.), Timed interfaces, No. 2491, 108-122, (2002), Berlin · Zbl 1027.68785
[22] Alfaro, L; Amadio, RM (ed.); Lugiez, D (ed.), Quantitative verification and control via the mu-calculus, 102-126, (2003), Berlin
[23] Alfaro, L; Faella, M; Henzinger, TA; Majumdar, R; Stoelinga, M, Model checking discounted temporal properties, Theor Comput Sci, 345, 139-170, (2005) · Zbl 1079.68062
[24] Alfaro, L; Faella, M; Stoelinga, M, Linear and branching system metrics, IEEE Trans Softw Eng, 35, 258-273, (2009) · Zbl 1098.68092
[25] de Alfaro L, Henzinger TA (2001) Interface automata. In: ESEC/SIGSOFT FSE. ACM, pp 109-120
[26] Delahaye B, Larsen KG, Legay A, Pedersen ML, Wąsowski A (2012) Consistency and refinement for interval Markov chains. J Log Algebr Program 81(3):209-226 · Zbl 1247.68195
[27] Delahaye B, Fahrenberg U, Larsen KG, Legay A (2014) Refinement and difference for probabilistic automata. Log Methods Comput Sci 10(3). doi:10.2168/LMCS-10(3:11)2014 · Zbl 1338.68144
[28] Desharnais, J; Gupta, V; Jagadeesan, R; Panangaden, P, Metrics for labelled Markov processes, Theor Comput Sci, 318, 323-354, (2004) · Zbl 1068.68093
[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 U, Legay A, Traonouez L-M (2014b) Structural refinement for the modal nu-calculus. In: Ciobanu G, Méry D (eds) ICTAC, volume 8687 of Lecture Notes in Computer Science. Springer, Berlin, pp 169-187 · Zbl 1432.68261
[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 · Zbl 1398.68339
[32] Fahrenberg U, Legay A (2012) A robust specification theory for modal event-clock automata. In: Bauer SS, Raclet J-B (eds) FIT, volume 87 of EPTCS. pp 5-16
[33] Fahrenberg, U; Legay, A; Shan, C-C (ed.), Generalized quantitative analysis of metric transition systems, 192-208, (2013), Berlin · Zbl 1426.68170
[34] Fahrenberg U, Legay A (2014a) General quantitative specification theories with modal transition systems. Acta Inform 51(5):261-295 · Zbl 1360.68585
[35] Fahrenberg U, Legay A (2014b) The quantitative linear-time-branching-time spectrum. Theor Comput Sci 538:54-69 · Zbl 1359.68191
[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 · Zbl 1246.68153
[37] Feuillade, G; Pinchinat, S, Modal specifications for the control theory of discrete event systems, Discrete Event Dyn Syst, 17, 211-232, (2007) · Zbl 1116.93037
[38] Girard, J-Y, Linear logic, Theor Comput Sci, 50, 1-102, (1987) · Zbl 0625.03037
[39] Hennessy, M, Acceptance trees, J ACM, 32, 896-928, (1985) · Zbl 0633.68074
[40] Henzinger, TA; Majumdar, R; Prabhu, VS; Pettersson, P (ed.); Yi, W (ed.), Quantifying similarities between timed systems, 226-241, (2005), Berlin · Zbl 1175.68281
[41] Henzinger, TA; Sifakis, J; Misra, J (ed.); Nipkow, T (ed.); Sekerinski, E (ed.), The embedded systems design challenge, 1-15, (2006), Berlin
[42] Huth M, Kwiatkowska MZ (1997) Quantitative analysis and model checking. In: LICS. IEEE Computer Society, pp 111-122
[43] Jacobs, B; Poll, E; Hußmann, H (ed.), A logic for the Java modeling language JML, 284-299, (2001), Berlin · Zbl 0977.68588
[44] Jonsson B, Larsen KG (1991) Specification and refinement of probabilistic processes. In: LICS. IEEE Computer Society, pp 266-277
[45] Klin, B; Sassone, V, Structural operational semantics for stochastic and weighted transition systems, Inf Comput, 227, 58-83, (2013) · Zbl 1358.68214
[46] Kozen, D, Results on the propositional \(μ \)-calculus, Theor Comput Sci, 27, 333-354, (1983) · Zbl 0553.03007
[47] Křetínský, J; Sickert, S; Hung, D (ed.); Ogawa, M (ed.), Motras: a tool for modal transition systems and their extensions, 487-491, (2013), Berlin · Zbl 1410.68232
[48] Larsen KG, Thomsen B (1998) A modal process logic. In: LICS. IEEE Computer Society, pp 203-210
[49] Larsen KG, Xinxin L (1990) Equation solving using modal transition systems. In: LICS. IEEE Computer Society, pp 108-117
[50] Larsen, KG, Proof systems for satisfiability in hennessy-milner logic with recursion, Theor Comput Sci, 72, 265-288, (1990) · Zbl 0698.68014
[51] Larsen, KG; Legay, A; Traonouez, L-M; Wąsowski, A; Fahrenberg, U (ed.); Tripakis, S (ed.), Robust specification of real time components, 129-144, (2011), Berlin
[52] Larsen, KG; Mardare, R; Panangaden, P; Rovan, B (ed.); Sassone, V (ed.); Widmayer, P (ed.), Taking it to the limit: approximate reasoning for Markov processes, 681-692, (2012), Berlin · Zbl 1365.68344
[53] Larsen, KG; Legay, A; Traonouez, L-M; Wąsowski, A, Robust synthesis for real-time systems, Theor Comput Sci, 515, 96-122, (2014) · Zbl 1311.68088
[54] Liskov, B; Wing, JM, A behavioral notion of subtyping, ACM Trans Program Lang Syst, 16, 1811-1841, (1994)
[55] Mio, M; Hofmann, M (ed.), Probabilistic modal mu-calculus with independent product, 290-304, (2011), Berlin · Zbl 1326.68202
[56] Morgan C, McIver A (1997) A probabilistic temporal calculus based on expectations. In: Groves L, Reeves S (eds) Formal methods. Springer, Singapore · Zbl 0885.03037
[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 · Zbl 1394.68219
[60] Sifakis, J, A vision for computer science-the system perspective, Cent Eur J Comput Sci, 1, 108-116, (2011)
[61] Traonouez L-M (2012) A parametric counterexample refinement approach for robust timed specifications. In Bauer SS, Raclet J-B (eds) FIT, volume 87 of EPTCS. pp 17-33
[62] Uchitel, S; Chechik, M; Taylor, RN (ed.); Dwyer, MB (ed.), Merging partial behavioural models, 43-52, (2004), New York
[63] Breugel, F; Worrell, J, A behavioural pseudometric for probabilistic transition systems, Theor Comput Sci, 331, 115-142, (2005) · Zbl 1070.68109
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.