Hostname: page-component-7c8c6479df-fqc5m Total loading time: 0 Render date: 2024-03-29T07:54:31.235Z Has data issue: false hasContentIssue false

Extending modal transition systems with structured labels

Published online by Cambridge University Press:  08 May 2012

SEBASTIAN S. BAUER
Affiliation:
Institut für Informatik, Ludwig-Maximilians-Universität München, München, Germany Email: bauerse@pst.ifi.lmu.de
LINE JUHL
Affiliation:
Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220 Aalborg Ø, Denmark Email: linej@cs.aau.dk
KIM G. LARSEN
Affiliation:
Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220 Aalborg Ø, Denmark Email: kgl@cs.aau.dk
AXEL LEGAY
Affiliation:
INRIA/IRISA, Rennes, France Email: axel.legay@irisa.fr
JIŘÍ SRBA
Affiliation:
Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220 Aalborg Ø, Denmark Email: srba@cs.aau.dk

Abstract

We introduce a novel formalism of label-structured modal transition systems that combines the classical may/must modalities on transitions with structured labels that represent quantitative aspects of the model. On the one hand, the specification formalism is general enough to include models like weighted modal transition systems and allows system developers to employ more complex label refinement than in previously studied theories. On the other hand, the formalism maintains the desirable properties required by any specification theory supporting compositional reasoning. In particular, we study modal and thorough refinement, determinisation, parallel composition, conjunction, quotient and logical characterisation of label-structured modal transition systems.

Type
Paper
Copyright
Copyright © Cambridge University Press 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Adler, B. T., de Alfaro, L., da Silva, L. D., Faella, M., Legay, A., Raman, V., and Roy, P. (2006) Ticc: A tool for interface compatibility and composition. In: Proceedings 18th International Conference on Computer Aided Verification (CAV). Springer-Verlag Lecture Notes in Computer Science 4144 5962.CrossRefGoogle Scholar
Antonik, A. and Huth, M. (2006) Efficient patterns for model checking partial state spaces in CTL ∩ LTL. Electronic Notes in Theoretical Computer Science 158 (0)4157.CrossRefGoogle Scholar
Bauer, S. S., Mayer, P., Schroeder, A. and Hennicker, R. (2010) On weak modal compatibility, refinement, and the mio workbench. In: Esparza, J. and Majumdar, R. (eds.) TACAS. Springer-Verlag Lecture Notes in Computer Science 6015 175189.CrossRefGoogle Scholar
Beneš, N., Křetínský, J., Larsen, K. G. and Srba, J. (2009a) Checking thorough refinement on modal transition systems is exptime-complete. In: Leucker, M. and Morgan, C. (eds.) ICTAC. Springer-Verlag Lecture Notes in Computer Science 5684 112126.CrossRefGoogle Scholar
Beneš, N., Křetínský, J., Larsen, K. G. and Srba, J. (2009b) On determinism in modal transition systems. Theoretical Computer Science 410 (41)40264043.CrossRefGoogle Scholar
Bertrand, N., Legay, A., Pinchinat, S. and Raclet, J.-B. (2009a) A compositional approach on modal specifications for timed systems. In: Breitman, K. and Cavalcanti, A. (eds.) ICFEM. Springer-Verlag Lecture Notes in Computer Science 5885 679697.CrossRefGoogle Scholar
Bertrand, N., Pinchinat, S. and Raclet, J.-B. (2009b) Refinement and consistency of timed modal specifications. In: Dediu, A. H., Ionescu, A.-M. and Martín-Vide, C. (eds.) LATA. Springer-Verlag Lecture Notes in Computer Science 5457 152163.CrossRefGoogle Scholar
Boudol, G. and Larsen, K. G. (1992) Graphical versus logical specifications. Theoretical Computer Science 106 (1)320.CrossRefGoogle Scholar
Bruns, G. and Godefroid, P. (2000) Generalized model checking: Reasoning about partial state spaces. In Palamidessi, C. (ed.) Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00). Springer-Verlag Lecture Notes in Computer Science 1877 168182.CrossRefGoogle Scholar
Caillaud, B., Delahaye, B., Larsen, K. G., Legay, A., Pedersen, M. L. and Wasowski, A. (2010) Compositional design methodology with constraint Markov chains. In: Proceedings of 7th International Conference on Quantitative Evaluation of SysTems (QEST), IEEE Computer Society 123132.Google Scholar
David, A., Larsen, K. G., Legay, A., Nyman, U. and Wasowski, A. (2010) Timed i/o automata: a complete specification theory for real-time systems. In: Johansson, K. H. and Yi, W. (eds.) HSCC, ACM 91100.Google Scholar
de Alfaro, L. and Henzinger, T. A. (2001) Interface automata. In: Proceedings of the 8th ESEC and 9th ACM SIGSOFT FSE, ACM 109120.Google Scholar
de Alfaro, L. and Henzinger, T. A. (2005) Interface-based Design. In: Broy, M., Grünbauer, J., Harel, D. and Hoare, C. A. R. (eds.) Engineering Theories of Software-intensive Systems, NATO Science Series: Mathematics, Physics, and Chemistry 195, Springer-Verlag 83104.CrossRefGoogle Scholar
de Alfaro, L., da Silva, L. D., Faella, M., Legay, A., Roy, P. and Sorea, M. (2005) Sociable interfaces. In: Proceedings 5th International Conference on Frontiers of Combining Systems (FROCOS). Springer-Verlag Lecture Notes in Computer Science 3717 81105.CrossRefGoogle Scholar
de Alfaro, L., Henzinger, T. A. and Stoelinga, M. (2002) Timed interfaces. In: Sangiovanni-Vincentelli, A. L. and Sifakis, J. (eds.) EMSOFT. Springer-Verlag Lecture Notes in Computer Science 2491 108122.CrossRefGoogle Scholar
Delahaye, B., Katoen, J.-P., Larsen, K. G., Legay, A., Pedersen, M. L., Sher, F. and Wasowski, A. (2011) Abstract probabilistic automata. In: Jhala, R. and Schmidt, D. (eds.) Proceedings of 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer-Verlag Lecture Notes in Computer Science 6538 324339.CrossRefGoogle Scholar
Delahaye, B., Larsen, K., Legay, A. and Wasowski, A. (2010) On greatest lower bound of modal transition systems. Technical report, INRIA.Google Scholar
Feuillade, G. and Pinchinat, S. (2007) Modal specifications for the control theory of discrete event systems. Discrete Event Dynamic Systems 17 (2)211232.CrossRefGoogle Scholar
Fischbein, D., Uchitel, S. and Braberman, V. (2006) A foundation for behavioural conformance in software product line architectures. In: Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis (ROSATEA'06), ACM 3948.CrossRefGoogle Scholar
Godefroid, P., Huth, M. and Jagadeesan, R. (2001) Abstraction-based model checking using modal transition systems. In: Larsen, K. G. and Nielsen, M. (eds.) CONCUR. Springer-Verlag Lecture Notes in Computer Science 2154 426440.CrossRefGoogle Scholar
Gordon, M. (1979) The Denotational Description of Programming Languages, Springer-Verlag.CrossRefGoogle Scholar
Gruler, A., Leucker, M. and Scheidemann, K. D. (2008) Calculating and modeling common parts of software product lines. In: SPLC, IEEE Computer Society 203212.Google Scholar
Hennessy, M. and Milner, R. (1985) Algebraic laws for non-determinism and concurrency. Journal of the ACM 32 (1)137161.CrossRefGoogle Scholar
Hoare, C. A. R. (1969) An axiomatic basis for computer programming. Communications of the ACM 12 576580.CrossRefGoogle Scholar
Hoare, C. A. R. (1985) Communicating Sequential Processes, Prentice-Hall.Google Scholar
Juhl, L., Larsen, K. G. and Srba, J. (2010) Modal Transition Systems with Weight Intervals.Google Scholar
Katoen, J.-P., Klink, D. and Neuhäußer, M. R. (2009) Compositional abstraction for stochastic systems. In: Ouaknine, J. and Vaandrager, F. W. (eds.) FORMATS. Springer-Verlag Lecture Notes in Computer Science 5813 195211.CrossRefGoogle Scholar
Larsen, K. G. (1985) A context dependent equivalence between processes. In: Brauer, W. (ed.) ICALP. Springer-Verlag Lecture Notes in Computer Science 194 373382.CrossRefGoogle Scholar
Larsen, K. G. (1987) A context dependent equivalence between processes. Theoretical Computer Science 49 184215.CrossRefGoogle Scholar
Larsen, K. G. (1989) Modal specifications. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems, Proceedings International Workshop, Grenoble, France. Springer-Verlag Lecture Notes in Computer Science 407 232246.CrossRefGoogle Scholar
Larsen, K. G. and Milner, R. (1987) Verifying a protocol using relativized bisimulation. In: Ottmann, T. (ed.) ICALP. Springer-Verlag Lecture Notes in Computer Science 267 126135.CrossRefGoogle Scholar
Larsen, K. G. and Milner, R. (1992) A compositional protocol verification using relativized bisimulation. Information and Computing 99 (1)80108.CrossRefGoogle Scholar
Larsen, K. G. and Thomsen, B. (1988a) Compositional proofs by partial specification of processes. In: Chytil, M., Janiga, L. and Koubek, V. (eds.) MFCS. Springer-Verlag Lecture Notes in Computer Science 324 414423.CrossRefGoogle Scholar
Larsen, K. G. and Thomsen, B. (1988b) A modal process logic. In: LICS, IEEE Computer Society 203210.Google Scholar
Larsen, K. G., Larsen, U. and Wasowski, A. (2005) Color-blind specifications for transformations of reactive synchronous programs. In: Cerioli, M. (ed.) FASE Springer-Verlag Lecture Notes in Computer Science 3442 160174.CrossRefGoogle Scholar
Larsen, K. G., Mikucionis, M. and Nielsen, B. (2004) Online testing of real-time systems using uppaal. In: Grabowski, J. and Nielsen, B. (eds.) FATES. Springer-Verlag Lecture Notes in Computer Science 3395 7994.CrossRefGoogle Scholar
Larsen, K. G., Nyman, U. and Wasowski, A. (2007) Modal i/o automata for interface and product line theories. In: Nicola, R. D. (ed.) ESOP. Springer-Verlag Lecture Notes in Computer Science 4421 6479.CrossRefGoogle Scholar
Milner, R. (1980) A Calculus of Communicating Systems. Springer-Verlag Lecture Notes in Computer Science 92.CrossRefGoogle Scholar
Milner, R. (1983) Calculi for synchrony and asynchrony. Theoretical Computer Science 25 267310.CrossRefGoogle Scholar
Park, D. M. R. (1981) Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) Proceedings of the 5th GI-Conference on Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 104 167183.CrossRefGoogle Scholar
Pierce, B. C. and Sangiorgi, D. (2000) Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM 47 531584.CrossRefGoogle Scholar
Plotkin, G. (1981) A structural approach to operational semantics. FN 19, DAIMI. Computer Science Department, Aarhus University, Denmark.Google Scholar
Raclet, J.-B. (2008) Residual for component specifications. In: Proceedings of the 4th International Workshop on Formal Aspects of Component Software (FACS'07). Electronic Notes in Theoretical Computer Science 215 93110.CrossRefGoogle Scholar
Stirling, C. (1987) Modal logics for communicating systems. Theoretical Computer Science 49 311347.CrossRefGoogle Scholar
Stirling, C. and Walker, D. (1989) CCS, liveness, and local model checking in the linear time mu-calculus. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems, Proceedings International Workshop, Grenoble, France. Springer-Verlag Lecture Notes in Computer Science 407 166178.CrossRefGoogle Scholar
Stoy, J. (1977) Denotational Semantics: The Scott–Strachey Approach to Progamming Language Theory, MIT Press.Google Scholar
van Glabbeek, R. J. (1990) The linear time-branching time spectrum (extended abstract). In: Baeten, J. C. M. and Klop, J. W. (eds.) CONCUR. Springer-Verlag Lecture Notes in Computer Science 458 278297.CrossRefGoogle Scholar