Axiomatisation and decidability of multi-dimensional Duration Calculus. (English) Zbl 1109.68069
Summary: The Shape Calculus is a spatio-temporal logic based on an \(n\)-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in \(n\)-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | M. Aiello, H. van Benthem, A Modal Walk Through Space, Tech. rep., Institute for Logic, Language and Computation, University of Amsterdam, 2001.; M. Aiello, H. van Benthem, A Modal Walk Through Space, Tech. rep., Institute for Logic, Language and Computation, University of Amsterdam, 2001. |
| [2] | Alur, R.; Dill, D. L., A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235 (1994) · Zbl 0803.68071 |
| [3] | Alur, R.; Henzinger, T. A., A really temporal logic, J. ACM, 41, 1, 181-204 (1994) · Zbl 0807.68065 |
| [4] | Behrmann, G.; David, A.; Larsen, K. G., A tutorial on uppaal, (Bernardo, M.; Corradini, F., Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Lecture Notes in Computer Science, vol. 3185 (2004), Springer-Verlag: Springer-Verlag Berlin), 200-236 · Zbl 1105.68350 |
| [5] | Bengtsson, J.; Yi, W., Timed automata: semantics, algorithms and tools, (Desel, J.; Reisig, W.; Rozenberg, G., Lectures on Concurrency and Petri Nets. Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, vol. 3098 (2003), Springer: Springer Berlin), 87-124 · Zbl 1088.68119 |
| [6] | Bennett, B.; Cohn, A.; Wolter, F.; Zakharyaschev, M., Multi-dimensional multi-modal logics as a framework for spatio-temporal reasoning, Appl. Intell., 17, 3, 239-251 (2002) · Zbl 1051.03019 |
| [7] | Blackburn, P.; Seligman, J., Hybrid languages, J. Logic Lang. Inform., 4, 251-272 (1995) · Zbl 0847.03009 |
| [8] | Bozga, M.; Daws, C.; Maler, O.; Olivero, A.; Tripakis, S.; Yovine, S., Kronos: a model-checking tool for real-time systems, (Hu, A. J.; Vardi, M. Y., Proceedings of the 10th International Conference on Computer Aided Verification, Vancouver, Canada, vol. 1427 (1998), Springer-Verlag: Springer-Verlag Berlin), 546-550 |
| [9] | Caires, L.; Cardelli, L., A spatial logic for concurrency, Inform. Comput., 186, 2, 194-235 (2003) · Zbl 1068.03022 |
| [10] | Cardelli, L.; Gordon, A. D., Mobile ambients, Theor. Comput. Sci., 240, 1, 177-213 (2000) · Zbl 0954.68108 |
| [11] | Cardelli, L.; Gordon, A. D., Anytime, anywhere: modal logics for mobile ambients, (POPL 2000 (2000), ACM Press), 365-377 · Zbl 1323.68405 |
| [12] | Chaochen, Zhou; Hoare, C.; Ravn, A., A calculus of durations, IPL, 40, 5, 269-276 (1991) · Zbl 0743.68097 |
| [13] | Chaochen, Z.; Ravn, A.; Hansen, M., An extended duration calculus for hybrid real-time systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, vol. 736 (1993), Springer: Springer Berlin), 36-59 · Zbl 0825.00044 |
| [14] | Charatonik, W.; Talbot, J.-M., The decidability of model checking mobile ambients, (Fribourg, L., CSL. CSL, Lecture Notes in Computer Science, vol. 2142 (2001), Springer: Springer Berlin), 339-354 · Zbl 0999.68123 |
| [15] | Charatonik, W.; Dal-Zilio, S.; Gordon, A. D.; Mukhopadhyay, S.; Talbot, J.-M., The complexity of model checking mobile ambients, (Honsell, F.; Miculan, M., FoSSaCS. FoSSaCS, Lecture Notes in Computer Science, vol. 2030 (2001), Springer: Springer Berlin), 152-167 · Zbl 0978.68096 |
| [16] | Charatonik, W.; Dal-Zilio, S.; Gordon, A. D.; Mukhopadhyay, S.; Talbot, J.-M., Model checking mobile ambients, Theor. Comput. Sci., 308, 1-3, 277-331 (2003) · Zbl 1068.68081 |
| [17] | Craig, W., On axiomatizability within a system, J. Symb. Log., 18, 1, 30-32 (1953) · Zbl 0053.20101 |
| [18] | H. Dierks, Specification and Verification of Polling Real-Time Systems, Ph.D. thesis, University of Oldenburg (Jul. 1999).; H. Dierks, Specification and Verification of Polling Real-Time Systems, Ph.D. thesis, University of Oldenburg (Jul. 1999). · Zbl 0953.68087 |
| [19] | Dierks, H., PLC-automata: a new class of implementable real-time automata, Theor. Comput. Sci., 253, 1, 61-93 (2000) · Zbl 0954.68085 |
| [20] | B. Dutertre, Complete proof systems for first order interval temporal logic, in: LICS, IEEE Computer Society, 1995, pp. 36-43.; B. Dutertre, Complete proof systems for first order interval temporal logic, in: LICS, IEEE Computer Society, 1995, pp. 36-43. |
| [21] | Franceschet, M.; Montanari, A.; de Rijke, M., Model checking for combined logics with an application to mobile systems, Autom. Softw. Eng., 11, 3, 289-321 (2004) |
| [22] | Fränzle, M., Model-checking dense-time duration calculus, Formal Asp. Comput., 16, 2, 121-139 (2004) · Zbl 1084.68071 |
| [23] | Gabbay, D. M., Fibring Logics (1999), Oxford University Press: Oxford University Press Oxford · Zbl 0909.03001 |
| [24] | Gabbay, D.; Kurucz, A.; Wolter, F.; Zakharyaschev, M., Many-Dimensional Modal Logics: Theory and Applications (2003), Elsevier: Elsevier Amsterdam · Zbl 1051.03001 |
| [25] | A. Galton, Towards a qualitative theory of movement, in: Spatial Information Theory, 1995, pp. 377-396.; A. Galton, Towards a qualitative theory of movement, in: Spatial Information Theory, 1995, pp. 377-396. |
| [26] | D. Giammarresi, A. Restivo, Handbook of formal languages—beyond words, in: Two-Dimensional Languages, vol. 3, Springer, Berlin, 1997, pp. 215-267.; D. Giammarresi, A. Restivo, Handbook of formal languages—beyond words, in: Two-Dimensional Languages, vol. 3, Springer, Berlin, 1997, pp. 215-267. |
| [27] | Hansen, M. R.; Chaochen, Zhou, Duration calculus: logical foundations, Formal Asp. Comput., 9, 283-330 (1997) · Zbl 0887.68101 |
| [28] | M. R. Hansen, Zhou Chaochen, Duration Calculus: A Formal Approach to Real-Time Systems, EATCS: Monographs in Theoretical Computer Science, Springer, Berlin, 2004.; M. R. Hansen, Zhou Chaochen, Duration Calculus: A Formal Approach to Real-Time Systems, EATCS: Monographs in Theoretical Computer Science, Springer, Berlin, 2004. · Zbl 1071.68062 |
| [29] | K. Havelund, A. Skou, K. G. Larsen, K. Lund, Formal modeling and analysis of an audio/video protocol: an industrial case study using uppaa., in: IEEE Real-Time Systems Symposium, IEEE Computer Society, 1997, pp. 2-13.; K. Havelund, A. Skou, K. G. Larsen, K. Lund, Formal modeling and analysis of an audio/video protocol: an industrial case study using uppaa., in: IEEE Real-Time Systems Symposium, IEEE Computer Society, 1997, pp. 2-13. |
| [30] | T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems, in: LICS, IEEE Computer Society, 1992, pp. 394-406.; T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Symbolic model checking for real-time systems, in: LICS, IEEE Computer Society, 1992, pp. 394-406. · Zbl 0806.68080 |
| [31] | N. Klarlund, A. Møller, MONA Version 1.4 User Manual, Tech. rep., Department of Computer Science, University of Aarhus (January 2001).; N. Klarlund, A. Møller, MONA Version 1.4 User Manual, Tech. rep., Department of Computer Science, University of Aarhus (January 2001). |
| [32] | Krieg-Brückner, B.; Peleska, J.; Olderog, E.-R.; Baer, A., The UniForM Workbench, a universal development environment for formal methods, (Wing, J.; Woodcock, J.; Davies, J., FM’99—Formal Methods. FM’99—Formal Methods, Lecture Notes in Computer Science, vol. 1709 (1999), Springer: Springer Berlin), 1186-1205 |
| [33] | Lindahl, M.; Pettersson, P.; Yi, W., Formal design and analysis of a gear controller, (Steffen, B., TACAS. TACAS, Lecture Notes in Computer Science, vol. 1384 (1998), Springer: Springer Berlin), 281-297 |
| [34] | Merz, S.; Wirsing, M.; Zappe, J., A spatio-temporal logic for the specification and refinement of mobile systems, (Pezzè, M., FASE 2003, Warsaw, Poland. FASE 2003, Warsaw, Poland, Lecture Notes in Computer Science, vol. 2621 (2003), Springer: Springer Berlin), 87-1014 · Zbl 1032.03028 |
| [35] | Milner, R., Communicating and mobile systems: the π-calculus (1999), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0942.68002 |
| [36] | P. Pandya, Specifying and deciding quantified discrete-time duration calculus formulae using dcvalid, Tech. rep., Tata Institute of Fundamental Research (2000).; P. Pandya, Specifying and deciding quantified discrete-time duration calculus formulae using dcvalid, Tech. rep., Tata Institute of Fundamental Research (2000). |
| [37] | P. K. Pandya, D. V. Hung, Duration calculus of weakly monotonic time, in: A.P. Ravn, H. Rischel (Eds.), FTRTFT’98, Lyngby, Denmark, vol. 1998, Lecture Notes in Computer Science, Springer, Berlin, 1998, pp. 55-64.; P. K. Pandya, D. V. Hung, Duration calculus of weakly monotonic time, in: A.P. Ravn, H. Rischel (Eds.), FTRTFT’98, Lyngby, Denmark, vol. 1998, Lecture Notes in Computer Science, Springer, Berlin, 1998, pp. 55-64. |
| [38] | J.-D. Quesel, MoDiShCa: Model-Checking discrete Shape Calculus, Minor Thesis, University of Oldenburg (August 2005).; J.-D. Quesel, MoDiShCa: Model-Checking discrete Shape Calculus, Minor Thesis, University of Oldenburg (August 2005). |
| [39] | Randell, D. A.; Cui, Z.; Cohn, A., A spatial logic based on regions and connection, (Nebel, B.; Rich, C.; Swartout, W., KR’92 (1992), Morgan Kaufmann: Morgan Kaufmann San Mateo, California), 165-176 |
| [40] | Reif, J. H.; Sistla, A. P., A multiprocess network logic with temporal and spatial modalities, J. Comput. Syst. Sci., 30, 1, 41-53 (1985) · Zbl 0565.68031 |
| [41] | Rudin, W., Principles of Mathematical Analysis (1964), McGraw-Hill: McGraw-Hill New York · Zbl 0148.02903 |
| [42] | Schäfer, A., A calculus for shapes in time and space, (Liu, Z.; Araki, K., Theoretical Aspects of Computing, ICTAC 2004. Theoretical Aspects of Computing, ICTAC 2004, Lecture Notes in Computer Science, vol. 3407 (2005), Springer), 463-478 · Zbl 1109.68068 |
| [43] | A. Schäfer, Axiomatisation and decidability of multi-dimensional duration calculus, in: J. Chomicki, D. Toman (Eds.), Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, TIME 2005, IEEE Computer Society, 2005, pp. 122-130.; A. Schäfer, Axiomatisation and decidability of multi-dimensional duration calculus, in: J. Chomicki, D. Toman (Eds.), Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, TIME 2005, IEEE Computer Society, 2005, pp. 122-130. |
| [44] | H. Vieira, L. Caires, The spatial logic model checker user’s manual, Tech. rep., Departamento de Informatica, FCT/UNL, tR-DI/FCT/UNL-03/2004 (2005).; H. Vieira, L. Caires, The spatial logic model checker user’s manual, Tech. rep., Departamento de Informatica, FCT/UNL, tR-DI/FCT/UNL-03/2004 (2005). |
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.
