×

Modal transition systems with weight intervals. (English) Zbl 1243.68215

Summary: We propose weighted modal transition systems, an extension to the well-studied specification formalism of modal transition systems that allows to express both required and optional behaviours of their intended implementations. In our extension we decorate each transition with a weight interval that indicates the range of concrete weight values available to the potential implementations. In this way resource constraints can be modelled using the modal approach. We focus on two problems. First, we study the question of existence/finding the largest common refinement for a number of finite deterministic specifications and we show PSPACE-completeness of this problem. By constructing the most general common refinement, we allow for a stepwise and iterative construction of a common implementation. Second, we study a logical characterisation of the formalism and show that a formula in a natural weight extension of the logic CTL is satisfied by a given modal specification if and only if it is satisfied by all its refinements. The weight extension is general enough to express different sorts of properties that we want our weights to satisfy.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

ACTLW
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Antonik, A.; Huth, M.; Larsen, K. G.; Nyman, U.; Wąsowski, A., 20 Years of modal and mixed specifications, Bull. EATCS, 95, 94-129 (2008) · Zbl 1169.68498
[2] Baier, C.; Katoen, J.-P., Principles of Model Checking (2008), The MIT Press
[3] Beneš, N.; Křetı´nský, J.; Larsen, K. G.; Srba, J., On determinism in modal transition systems, Theoret. Comput. Sci., 410, 41, 4026-4043 (2009) · Zbl 1186.68314
[4] Beneš, N.; Křetı´nský, J.; Larsen, K. G.; Srba, J., Checking thorough refinement on modal transition systems is EXPTIME-complete, (Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC’09). Proceedings of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC’09), LNCS, vol. 5684 (2009), Springer-Verlag), 112-126 · Zbl 1250.68117
[5] Bertrand, N.; Pinchinat, S.; Raclet, J.-B., Refinement and consistency of timed modal specifications, (Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA’09). Proceedings of the 3rd International Conference on Language and Automata Theory and Applications (LATA’09), LNCS, vol. 5457 (2009), Springer-Verlag), 152-163 · Zbl 1234.68250
[6] Bouyer, P.; Fahrenberg, U.; Larsen, K. G.; Markey, N.; Srba, J., Infinite runs in weighted timed automata with energy constraints, (Cassez, F.; Jard, C., Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’08). Proceedings of the 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS’08), LNCS, vol. 5215 (2008), Springer-Verlag: Springer-Verlag Saint-Malo, France), 33-47 · Zbl 1171.68524
[7] Bruns, G.; Godefroid, P., Generalized model checking: reasoning about partial state spaces, (Palamidessi, C., Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’00). Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’00), LNCS, vol. 1877 (2000), Springer-Verlag), 168-182 · Zbl 0999.68524
[8] Droste, M.; Gastin, P., Weighted automata and weighted logics, (Proceedings of the 7th International Colloquium on Automata, Languages and Programming (ICALP’05). Proceedings of the 7th International Colloquium on Automata, Languages and Programming (ICALP’05), LNCS, vol. 3580 (2005), Springer-Verlag), 513-525 · Zbl 1084.03036
[9] (Droste, M.; Kuich, W.; Vogler, H., Handbook of Weighted Automata (2009), Springer-Verlag) · Zbl 1200.68001
[10] Emerson, E. A.; Clarke, E. M., Characterizing correctness properties of parallel programs using fixpoints, (Proceedings of the 7th International Colloquium on Automata, Languages and Programming (ICALP’80). Proceedings of the 7th International Colloquium on Automata, Languages and Programming (ICALP’80), LNCS, vol. 85 (1980), Springer-Verlag), 169-181 · Zbl 0456.68016
[11] Fecher, H.; Schmidt, H., Comparing disjunctive modal transition systems with an one-selecting variant, J. Logic Algebr. Program., 77, 1-2, 20-39 (2008) · Zbl 1151.68035
[12] Godefroid, P.; Huth, M.; Jagadeesan, R., Abstraction-based model checking using modal transition systems, (Proceedings of the 12th International Conference on Concurrency Theory (CONCUR’01). Proceedings of the 12th International Conference on Concurrency Theory (CONCUR’01), LNCS, vol. 2154 (2001), Springer-Verlag), 426-440 · Zbl 1006.68077
[13] Gruler, A.; Leucker, M.; Scheidemann, K. D., Modeling and model checking software product lines, (Barthe, G.; de Boer, F. S., FMOODS. FMOODS, LNCS, vol. 5051 (2008), Springer-Verlag), 113-131
[14] Gruler, A.; Leucker, M.; Scheidemann, K. D., Calculating and modeling common parts of software product lines, (Proceedings of the 13th International Software Product Line Conference (SPLC’08) (2008), IEEE Computer Society), 203-212
[15] Henzinger, T.; Sifakis, J., The embedded systems design challenge, (Proceedings of the 14th International Symposium on Formal Methods (FM’06). Proceedings of the 14th International Symposium on Formal Methods (FM’06), LNCS, vol. 4085 (2006), Springer-Verlag), 1-15
[16] Henzinger, T. A.; Sifakis, J., The discipline of embedded systems design, IEEE Comput., 40, 10, 32-40 (2007)
[17] Huth, M.; Jagadeesan, R.; Schmidt, D. A., Modal transition systems: a foundation for three-valued program analysis, (Proceedings of the 10th European Symposium on Programming (ESOP’01). Proceedings of the 10th European Symposium on Programming (ESOP’01), LNCS, vol. 2028 (2001), Springer-Verlag), 155-169 · Zbl 0987.68849
[18] Kanellakis, P.; Smolka, S., CCS expressions, finite state processes, and three problems of equivalence, Inform. Comput., 86, 1, 43-68 (1990) · Zbl 0705.68063
[19] Larsen, K. G.; Thomsen, B., A modal process logic, (Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS’88) (1988), IEEE Computer Society), 203-210
[20] Lluch-Lafuente, A.; Montanari, U., Quantitative \(\mu \)-calculus and CTL defined over constraint semirings, Theoret. Comput. Sci., 346, 1, 135-160 (2005) · Zbl 1080.68065
[21] Meolic, R.; Kapus, T.; Brezocnik, Z., ACTLW - an action-based computation tree logic with unless operator, Inform. Sci., 178, 6, 1542-1557 (2008) · Zbl 1134.68033
[22] Nanz, S.; Nielson, F.; Nielson, H. R., Modal abstractions of concurrent behaviour, (Proceedings of 15th International Symposium on Static Analysis (SAS’08). Proceedings of 15th International Symposium on Static Analysis (SAS’08), LNCS, vol. 5079 (2008), Springer-Verlag), 159-173 · Zbl 1149.68407
[23] Nicola, R. D.; Vaandrager, F. W., Action versus state based logics for transition systems, (Semantics of Systems of Concurrent Processes. Semantics of Systems of Concurrent Processes, LNCS, vol. 469 (1990), Springer-Verlag), 407-419
[24] Paige, R.; Tarjan, R., Three partition refinement algorithms, SIAM J. Comput., 16, 6, 973-989 (1987) · Zbl 0654.68072
[25] Raclet, J.-B., Residual for component specifications, Electron. Notes Theoret. Comput. Sci., 215, 93-110 (2008)
[26] Raclet, J.-B.; Badouel, E.; Benveniste, A.; Caillaud, B.; Passerone, R., Why are modalities good for interface theories?, (Proceedings of the 9th International Conference on Application of Concurrency to System Design (ACSD’09) (2009), IEEE Computer Society: IEEE Computer Society Los Alamitos, CA, USA), 119-127
[27] Uchitel, S.; Chechik, M., Merging partial behavioural models, (Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineerings (FSE’04) (2004), ACM), 43-52
[28] Wei, O.; Gurfinkel, A.; Chechik, M., Mixed transition systems revisited, (Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’09). Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI’09), LNCS, vol. 5403 (2009), Springer-Verlag), 349-365 · Zbl 1206.68194
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.