Abstract
Duration Calculus (or DC in short) presents a formal notation to specify properties of real-time systems and a calculus to formally prove such properties. Decidability is the underlying foundation to automated reasoning. But, excepting some of its simple fragments, DC has been shown to be undecidable.
DC takes the set of real numbers to represent time. The main reason of undecidability comes from the assumption that, in a real-time system, state changes can occur at any time point. But an implementation of a specification (for a class of applications) is ultimately executed on a computer, and there states change according to a system clock. Under such an assumption, it has been shown that the decidability results can be extended to cover relatively richer subsets of DC. In this paper, we extend such decidability results to still richer subsets of DC.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bouajjani A., Lakhnech Y. & Robbana R., Prom Duration Calculus to Linear Hybrid Automata, Proc. of 7th Intnl. Conf. on Computaer Aided Verification (CAV ’95), LNCS No. 939, 1995.
Dutertre B., Complete Proof systems for First Order Interval Logic, Tenth Anual IEEE Symposium on Logic in Computer Science, pp. 36–43, IEEE Press, 1995.
FrÄnzle M., Controller Design from Temporal Logic: Undecidability need not matter, Dissertation, University of Kiel, 1996.
Hansen M.R. & Zhou Chaochen, Duration Calculus: Logical Foundations, To appear in Formal Aspects of Computing, Springer Verlag.
Joseph M., Real-Time Systems:Specification, Verification and Analysis, Printice Hall Intl. Series in Computer Science, 1996.
Ravn A.P., Rischel H. & Hansen K.M., Specifying and Verifying Requirements of Real-Time Systems, IEEE Tr. on Software Engineering, Vol 19(1), January 1993.
Satpathy M., Hung D.V. & Pandya P.K., Some Results on the Decidability of Duration Calculus under Synchronous Interpretation, TR No. 86, UNU/IIST, Macau, 1996.
Skakkebaek J.U., Ravn A.P., Rischel H. & Zhao Chao Chen, Specification of Embedded real-time systems, Proc. of Euromicro Workshop on real-time systems, IEEE Computer Society Press, 1992.
Skakkebaek J.U. & Sestoft P, Checking Validity of Duration Calculus Formulas, Report ID/DTH/ JUS 3/1, Technical University of Denmark, Denmark, 1994.
Yuhua Z. & Zhou Chaochen, A Formal Proof of the Deadline Driven Scheduler, Third International Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, Lubeck (Germany), LNCS No. 863, Springer Verlag, 1994, pp. 756–775.
Zhou Chaochen, Hoare C.A.R. & Ravn A.P., A calculus of durations, Information Processing Letters, Vol 40(5), pp. 269–276, 1991.
Zhou Chaochen, Hansen M.R. & Sestoft P, Decidability and Undecidability Results in Duration Calculus, Proc. of the 10th Annual Symposium on Theoretical Aspects of Computer Science (STACS 93), LNCS No. 665, Springer Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Satpathy, M., Van Hung, D., Pandya, P.K. (1998). Some decidability results for duration calculus under synchronous interpretation. In: Ravn, A.P., Rischel, H. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1998. Lecture Notes in Computer Science, vol 1486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055347
Download citation
DOI: https://doi.org/10.1007/BFb0055347
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65003-4
Online ISBN: 978-3-540-49792-9
eBook Packages: Springer Book Archive