TY - JOUR
T1 - Timed concurrent constraint programming
T2 - Decidability results and their application to LTL
AU - Valencia, Frank D.
PY - 2003
Y1 - 2003
N2 - 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) 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 wellestablished formalisms for concurrency.
AB - 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) 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 wellestablished formalisms for concurrency.
UR - http://www.scopus.com/inward/record.url?scp=0347526016&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-24599-5_29
DO - 10.1007/978-3-540-24599-5_29
M3 - Article
AN - SCOPUS:0347526016
SN - 0302-9743
VL - 2916
SP - 422
EP - 437
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ER -