Abstract
The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp). The ntcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problem is then whether the sequences in the sp of a given process satisfy a given ntcc LTL formula.
This paper presents new positive decidability results for timed ccp as well as for LTL. In particular, we shall prove that the following problems are decidable: (1) The sp equivalence for the so-called locally-independentntcc fragment; unlike other fragments for which similar results have been published, this fragment can specify infinite-state systems. (2) Verification for locally-independent processes and negation-free first-order formulae of the ntcc LTL. (3) Implication for such formulae. (4) Satisfiability for a first-order fragment of Manna and Pnueli’s LTL. The purpose of the last result is to illustrate the applicability of ccp to well-established formalisms for concurrency.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M.: The power of temporal proofs. Theoretical Computer Science 65, 35–84 (1989)
Buchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Conf. on Logic, Methodology, and Philosophy of Science, pp. 1–11 (1962)
Choueka, Y.: Theories of automata on ω-tapes:A simplified approach. Computer and System Sciences 10, 19–35 (1974)
de Boer, F., Gabbrielli, M., Meo, M.C.: Atimed concurrent constraint language. Information and Computation 161, 45–83 (2000)
de Boer, F., Gabbrielli, M., Marchiori, E., Palamidessi, C.: Proving concurrent constraint programs correct. ACM Transactions on Programming Languages and Systems 19(5) (1997)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 223. Springer, Heidelberg (1999)
Esparza, J., Melzer, S.: Model checking LTL using constraint programming. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248. Springer, Heidelberg (1997)
Falaschi, M., Policriti, A., Villanueva, A.: Modelling timed concurrent systems in a temporal concurrent constraint language - I. ENTCS, vol. 48 (2001)
Hodkinson, I., Wolter, F., Zakharyasche, M.: Decidable fragments of first-order temporal logic. Ann. Pure. Appl. Logic 106, 85–134 (2000)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Specification. Springer, Heidelberg (1991)
Merz, S.: Decidability and incompleteness results for first-order temporal logics of linear time. Journal of Applied Non-Classical Logic 2(2) (1992)
Milner, R.: A finite delay operator in synchronous ccs. TR CSR-116-82, Univ. of Edinburgh
Milner, R.: Communicating and Mobile Systems: the π-calculus (1999)
Nielsen, M., Palamidessi, C., Valencia, F.: On the expressive power of concurrent constraint programming languages. In: PPDP 2002, October 2002, pp. 156–167. ACM Press, New York (2002)
Nielsen, M., Palamidessi, C., Valencia, F.: Temporal concurrent constraint programming: Denotation, logic and applications. Nordic Journal of Computing 9(2), 145–188 (2002)
Nielsen, M., Valencia, F.: Temporal Concurrent Constraint Programming: Applications and Behavior. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, pp. 298–324. Springer, Heidelberg (2002)
Palamidessi, C., Valencia, F.: A temporal concurrent constraint programming calculus. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, p. 302. Springer, Heidelberg (2001)
Saraswat, V., Jagadeesan, R., Gupta, V.: Foundations of timed concurrent constraint programming. In: Proc. of LICS 1994, pp. 71–80 (1994)
Saraswat, V., Jagadeesan, R., Gupta, V.: Programming in timed concurrent constraint languages. In: Constraint Programming: Proc. 1993, pp. 361–410. Springer, Heidelberg (1994)
Saraswat, V., Jagadeesan, R., Gupta, V.: Timed default concurrent constraint programming. Journal of Symbolic Computation 22, 475–520 (1996)
Saraswat, V., Rinard, M., Panangaden, P.: The semantic foundations of concurrent constraint programming. In: POPL 1991, pp. 333–352 (1991)
Sistla, A., Vardi, M., Wolper, P.: The complementation problem for buchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)
Tini, S.: On the expressiveness of timed concurrent constraint programming. ENTCS, vol. 27 (1999)
Valencia, F.: Temporal Concurrent Constraint Programming. PhD thesis, BRICS Univ. of Aarhus (2003), Available online via http://www.brics.dk/~fvalenci/publications.html
Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valencia, F.D. (2003). Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL. In: Palamidessi, C. (eds) Logic Programming. ICLP 2003. Lecture Notes in Computer Science, vol 2916. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24599-5_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-24599-5_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20642-2
Online ISBN: 978-3-540-24599-5
eBook Packages: Springer Book Archive