On the completeness and decidability of duration calculus with iteration. (English) Zbl 1108.68074
Summary: The extension of the Duration Calculus (DC) by iteration, which is also known as Kleene star, enables the straightforward specification of repetitive behaviour in DC and facilitates the translation of design descriptions between DC, timed regular expressions and timed automata. In this paper we present axioms and a proof rule about iteration in DC. We consider abstract-time DC and its extension by a state-variable binding existential quantifier known as Higher-order DC (HDC). We show that the \(\omega\)-complete proof systems for DC and HDC known from our earlier work can be extended by our axioms and rule in various ways in order to axiomatise iteration completely. The additions we propose include either the proof rule or an induction axiom. We also present results on the decidability of a subset of the extension DC\(^*\) of DC by iteration.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B25 | Decidability of theories and sets of sentences |
| 68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
References:
| [1] | S. Abramsky, D. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, Clarendon Press, Oxford, 1992.; S. Abramsky, D. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, Clarendon Press, Oxford, 1992. · Zbl 0777.68001 |
| [2] | Alur, R.; Dill, D. L., A theory of timed automata, Theoret. Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071 |
| [3] | E. Asarin, P. Caspi, O. Maler, A Kleene theorem for timed automata, in: G. Winskel (Ed.), Proc. IEEE Internat. Symp. Logics in Computer Science LICS’97, IEEE Computer Society Press, Silver Spring, MD, 1997, pp. 160-171.; E. Asarin, P. Caspi, O. Maler, A Kleene theorem for timed automata, in: G. Winskel (Ed.), Proc. IEEE Internat. Symp. Logics in Computer Science LICS’97, IEEE Computer Society Press, Silver Spring, MD, 1997, pp. 160-171. |
| [4] | Dang Van Hung, Modelling and verification of biphase mark protocols in duration calculus using PVS/DC \({}^-\); Dang Van Hung, Modelling and verification of biphase mark protocols in duration calculus using PVS/DC \({}^-\) |
| [5] | Dang Van Hung, D.P. Guelev, Completeness and decidability of a fragment of duration calculus with iteration, in: P.S. Thiagarajan, R. Yap (Eds.), Advances in Computing Science—ASIAN’99, Vol. 1742, Springer, Berlin, 1999, pp. 139-150.; Dang Van Hung, D.P. Guelev, Completeness and decidability of a fragment of duration calculus with iteration, in: P.S. Thiagarajan, R. Yap (Eds.), Advances in Computing Science—ASIAN’99, Vol. 1742, Springer, Berlin, 1999, pp. 139-150. · Zbl 0954.03033 |
| [6] | Dang Van Hung, Pham Hong Thai, On checking parallel real-time systems for linear duration invariants, in: B. Kramer, N. Uchihita, P. Croll, S. Russo (Eds.), Proc. Internat. Symp. of Software Engineering for Parallel and Distributed Systems (PDSE’98), IEEE Computer Society Press, Silver Spring, MD, April 1998, pp. 61-71.; Dang Van Hung, Pham Hong Thai, On checking parallel real-time systems for linear duration invariants, in: B. Kramer, N. Uchihita, P. Croll, S. Russo (Eds.), Proc. Internat. Symp. of Software Engineering for Parallel and Distributed Systems (PDSE’98), IEEE Computer Society Press, Silver Spring, MD, April 1998, pp. 61-71. |
| [7] | Dang Van Hung, Wang Ji, On the design of hybrid control systems using automata models, in: Proc. FST TCS 1996, Lecture Notes in Computer Science, Vol. 1180, Springer, Berlin, 1996, pp. 156-167.; Dang Van Hung, Wang Ji, On the design of hybrid control systems using automata models, in: Proc. FST TCS 1996, Lecture Notes in Computer Science, Vol. 1180, Springer, Berlin, 1996, pp. 156-167. · Zbl 1541.68214 |
| [8] | B. Dutertre, On first-order interval temporal logic, Report CSD-TR-94-3, Department of Computer Science, Royal Holloway, University of London, Egham, Surrey TW20 0EX, England, 1995. (A short version appeared as [9]).; B. Dutertre, On first-order interval temporal logic, Report CSD-TR-94-3, Department of Computer Science, Royal Holloway, University of London, Egham, Surrey TW20 0EX, England, 1995. (A short version appeared as [9]). |
| [9] | B. Dutertre, On first order interval temporal logic, in: Proc. LICS’95, IEEE Computer Society Press, Silver Spring, MD, 1995, pp. 36-43.; B. Dutertre, On first order interval temporal logic, in: Proc. LICS’95, IEEE Computer Society Press, Silver Spring, MD, 1995, pp. 36-43. |
| [10] | D.P. Guelev, A calculus of durations on abstract domains: completeness and extensions, Technical Report 139, UNU/IIST, P.O. Box 3058, Macau, May 1998.; D.P. Guelev, A calculus of durations on abstract domains: completeness and extensions, Technical Report 139, UNU/IIST, P.O. Box 3058, Macau, May 1998. |
| [11] | D.P. Guelev, A complete fragment of higher-order duration \(\operatorname{Μ;} \); D.P. Guelev, A complete fragment of higher-order duration \(\operatorname{Μ;} \) · Zbl 1044.68108 |
| [12] | D.P. Guelev, Interpolation and related results on the \(\lceil; P \rceil; DC \); D.P. Guelev, Interpolation and related results on the \(\lceil; P \rceil; DC \) |
| [13] | D.P. Guelev, Probabilistic and temporal modal logics, Ph.D. Thesis, Sofia University, 2000 (in Bulgarian).; D.P. Guelev, Probabilistic and temporal modal logics, Ph.D. Thesis, Sofia University, 2000 (in Bulgarian). |
| [14] | Guelev, D. P., A complete proof system for first-order interval temporal logic with projection, J. Logic Comput., 14, 2, 215-249 (2004) · Zbl 1070.03009 |
| [15] | D.P. Guelev, Sharpening the incompleteness of the duration calculus, in: Irek Ulidowski (Ed.), Proc. ARTS 2004, volume? of ENTCS, Elsevier Science, Amsterdam, 2004 (Presented at ARTS 2004, Stirling, UK).; D.P. Guelev, Sharpening the incompleteness of the duration calculus, in: Irek Ulidowski (Ed.), Proc. ARTS 2004, volume? of ENTCS, Elsevier Science, Amsterdam, 2004 (Presented at ARTS 2004, Stirling, UK). · Zbl 1272.03140 |
| [16] | M.R. Hansen, Zhou Chaochen, Semantics and completeness of duration calculus, in: Real-Time: Theory and Practice, Lecture Notes in Computer Science, Vol. 600, Springer, Berlin, 1992, pp. 209-225.; M.R. Hansen, Zhou Chaochen, Semantics and completeness of duration calculus, in: Real-Time: Theory and Practice, Lecture Notes in Computer Science, Vol. 600, Springer, Berlin, 1992, pp. 209-225. |
| [17] | M.R. Hansen, Zhou Chaochen, Chopping a point, in: BCS-FACS Seventh Refinement Workshop, Electronic Workshops in Computing, Springer, Berlin, 1996.; M.R. Hansen, Zhou Chaochen, Chopping a point, in: BCS-FACS Seventh Refinement Workshop, Electronic Workshops in Computing, Springer, Berlin, 1996. |
| [18] | Hansen, M. R.; Zhou Chaochen, Duration calculuslogical foundations, Formal Aspects of Comput., 9, 283-330 (1997) · Zbl 0887.68101 |
| [19] | He Jifeng, A behavioral model for co-design, in: Proc. FM’99, Lecture Notes in Computer Science, Vol. 1709, Springer, Berlin, 1999, pp. 1420-1438.; He Jifeng, A behavioral model for co-design, in: Proc. FM’99, Lecture Notes in Computer Science, Vol. 1709, Springer, Berlin, 1999, pp. 1420-1438. · Zbl 0948.03511 |
| [20] | He Jifeng, Integrating variants of DC, Research Report 172, UNU/IIST, P.O. Box 3058, Macau, August 1999.; He Jifeng, Integrating variants of DC, Research Report 172, UNU/IIST, P.O. Box 3058, Macau, August 1999. |
| [21] | He Weidong; Zhou Chaochen, A case study of optimization, Comput. J., 38, 9, 734-746 (1995) |
| [22] | Kozen, D., Results on the propositional \(\mu \)-calculus, Theoret. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007 |
| [23] | Li Xuan Dong, Dang Van Hung, Checking linear duration invariants by linear programming, in: J. Jaffar, R.H.C. Yap (Eds.), Concurrency and Palalellism, Programming, Networking, and Security, Lecture Notes in Computer Science, Vol. 1179, Springer, Berlin, 1996, pp. 321-332.; Li Xuan Dong, Dang Van Hung, Checking linear duration invariants by linear programming, in: J. Jaffar, R.H.C. Yap (Eds.), Concurrency and Palalellism, Programming, Networking, and Security, Lecture Notes in Computer Science, Vol. 1179, Springer, Berlin, 1996, pp. 321-332. · Zbl 1541.68229 |
| [24] | Li Xuan Dong, Dang Van Hung, Zheng Tao, Checking hybrid automata for linear duration invariants, in: R.K. Shamasundar, K. Ueda (Eds.), Advances in Computing Science, Lecture Notes in Computer Science, Vol. 1345, Springer, Berlin, 1997, pp. 166-180.; Li Xuan Dong, Dang Van Hung, Zheng Tao, Checking hybrid automata for linear duration invariants, in: R.K. Shamasundar, K. Ueda (Eds.), Advances in Computing Science, Lecture Notes in Computer Science, Vol. 1345, Springer, Berlin, 1997, pp. 166-180. |
| [25] | Moszkowski, B., Temporal logic for multilevel reasoning about hardware, IEEE Comput., 18, 2, 10-19 (1985) |
| [26] | Moszkowski, B., Executing Temporal Logic Programs (1986), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0565.68003 |
| [27] | B. Moszkowski, A hierarchical completeness proof for propositional temporal logic, in: N. Dershowitz (Ed.), Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, Lecture Notes in Computer Science, Vol. 2772, Springer, Berlin, 2003, pp. 480-523.; B. Moszkowski, A hierarchical completeness proof for propositional temporal logic, in: N. Dershowitz (Ed.), Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, Lecture Notes in Computer Science, Vol. 2772, Springer, Berlin, 2003, pp. 480-523. · Zbl 1274.03034 |
| [28] | P.K. Pandya, Some extensions to mean-value calculus: expressiveness and decidability, in: Proc. CSL’95, Lecture Notes in Computer Science, Vol. 1092, Springer, Berlin, 1995, pp. 434-451.; P.K. Pandya, Some extensions to mean-value calculus: expressiveness and decidability, in: Proc. CSL’95, Lecture Notes in Computer Science, Vol. 1092, Springer, Berlin, 1995, pp. 434-451. |
| [29] | P.K. Pandya, Dang Van Hung, Duration calculus of weakly monotonic time, in: Proc. FTRTFT’98, Lecture Notes in Computer Science, Vol. 1486, Springer, Berlin, 1998, pp. 55-64.; P.K. Pandya, Dang Van Hung, Duration calculus of weakly monotonic time, in: Proc. FTRTFT’98, Lecture Notes in Computer Science, Vol. 1486, Springer, Berlin, 1998, pp. 55-64. |
| [30] | E. Pavlova, Dang Van Hung, A formal specification of the concurrency control in real-time databases, Technical Report 152, UNU/IIST, P.O. Box 3058, Macau, January 1999.; E. Pavlova, Dang Van Hung, A formal specification of the concurrency control in real-time databases, Technical Report 152, UNU/IIST, P.O. Box 3058, Macau, January 1999. |
| [31] | Shoenfield, J., Mathematical Logic (1967), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0155.01102 |
| [32] | Skordev, D., On the duration domains for interval temporal logic, Annuaire de l’Universite de Sofia “St. Kliment Ochriski”, 94, 27-33 (2000) · Zbl 1079.03529 |
| [33] | J.A.F.K. van Benthem, Modal Logic and Classical Logic, Bibliopolis, 1983.; J.A.F.K. van Benthem, Modal Logic and Classical Logic, Bibliopolis, 1983. · Zbl 0639.03014 |
| [34] | B.H. Widjaja, He Weidong, Chen Zongji, Zhou Chaochen, A cooperative design for hybrid systems, in: A. Pnueli, H. Lin (Eds.), Logic and Software Engineering, International Workshop in Honor of Chih-Sung Tang, World Scientific, Singapore, 1996, pp. 127-150.; B.H. Widjaja, He Weidong, Chen Zongji, Zhou Chaochen, A cooperative design for hybrid systems, in: A. Pnueli, H. Lin (Eds.), Logic and Software Engineering, International Workshop in Honor of Chih-Sung Tang, World Scientific, Singapore, 1996, pp. 127-150. |
| [35] | Xu Qiwen, He Weidong, Hierarchical design of a chemical concentration control system, in: Proc. Hybrid Systems III: Verification and Control, Lecture Notes in Computer Science, Vol. 1066, Springer, Berlin, 1995, pp. 270-281.; Xu Qiwen, He Weidong, Hierarchical design of a chemical concentration control system, in: Proc. Hybrid Systems III: Verification and Control, Lecture Notes in Computer Science, Vol. 1066, Springer, Berlin, 1995, pp. 270-281. |
| [36] | Yu Xinyao, Wang Ji, Zhou Chaochen, P.K. Pandya, Specification of an adaptive control system, in: Formal Techniques in Real-Time and Fault-Tolerant systems, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 738-755.; Yu Xinyao, Wang Ji, Zhou Chaochen, P.K. Pandya, Specification of an adaptive control system, in: Formal Techniques in Real-Time and Fault-Tolerant systems, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 738-755. |
| [37] | Zheng Yuhua, Zhou Chaochen, A formal proof of a deadline driven scheduler, in: Proc. FTRTFT’94, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 756-775.; Zheng Yuhua, Zhou Chaochen, A formal proof of a deadline driven scheduler, in: Proc. FTRTFT’94, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 756-775. |
| [38] | Zhou Chaochen, D.P. Guelev, Zhan Naijun, A Higher-order Duration Calculus, Palgrave, 2000, pp. 407-416.; Zhou Chaochen, D.P. Guelev, Zhan Naijun, A Higher-order Duration Calculus, Palgrave, 2000, pp. 407-416. |
| [39] | Zhou Chaochen; Hansen, M. R., Duration Calculus, A Formal Approach to Real-Time Systems (2004), Springer: Springer Berlin · Zbl 1071.68062 |
| [40] | Zhou Chaochen, M.R. Hansen, P. Sestoft, Decidability and undecidability results for duration calculus, in: STACS’93, Lecture Notes in Computer Science, Vol. 665, Springer, Berlin, 1993, pp. 58-68.; Zhou Chaochen, M.R. Hansen, P. Sestoft, Decidability and undecidability results for duration calculus, in: STACS’93, Lecture Notes in Computer Science, Vol. 665, Springer, Berlin, 1993, pp. 58-68. · Zbl 0811.68115 |
| [41] | Zhou Chaochen; Hoare, C. A.R.; Ravn, A. P., A calculus of durations, Inform. Process. Lett., 40, 5, 269-276 (1991) · Zbl 0743.68097 |
| [42] | Zhou Chaochen, Li Xiaoshan, A Mean Value Calculus of Durations, Prentice-Hall, Englewood Cliffs, NJ, 1994, pp. 431-451.; Zhou Chaochen, Li Xiaoshan, A Mean Value Calculus of Durations, Prentice-Hall, Englewood Cliffs, NJ, 1994, pp. 431-451. |
| [43] | Zhou Chaochen, Zhang Jingzhong, Yang Lu, Li Xiaoshan, Linear duration invariants, in: Proc. FTRTFT’94, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 86-109.; Zhou Chaochen, Zhang Jingzhong, Yang Lu, Li Xiaoshan, Linear duration invariants, in: Proc. FTRTFT’94, Lecture Notes in Computer Science, Vol. 863, Springer, Berlin, 1994, pp. 86-109. |
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.
