Sciweavers

Share
ICLP
2003
Springer

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

9 years 4 months ago
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...
Frank D. Valencia
Added 07 Jul 2010
Updated 07 Jul 2010
Type Conference
Year 2003
Where ICLP
Authors Frank D. Valencia
Comments (0)
books