Timed Concurrent Constraint Programming: Decidability Results and Their Application to LTL

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-independent ntcc 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) Satisfiabili...

• Type: Conference
• Year: 2003
• Where: ICLP
• Authors: Frank D. Valencia
• Keywords: ICLP 2003, Ntcc Ltl, Ntcc Ltl Formula, Programming Languages, Timed Concurrent Constraint