Decidability of infinite-state timed CCP processes and first-order LTL

作     者：Valencia, FD 

作者机构：Ecole Polytech LIX CNRS F-91128 Palaiseau France 

出 版 物：《THEORETICAL COMPUTER SCIENCE》 (理论计算机科学)

年 卷 期：2005年第330卷第3期

页      面：577-607页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：process calculi timed concurrent constraint programming infinite-state systems temporal logic first-order LTL decidability 

摘      要：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-orderformulae 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. (C) 2004 Elsevier B.V. All rights reserved.