Loading...
Please wait, while we are loading the content...
Similar Documents
On the Decidability of Timed CCP
| Content Provider | Semantic Scholar |
|---|---|
| Author | Valencia, Frank D. |
| Copyright Year | 2007 |
| Abstract | Thentcc 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 ob servation in ccp is the strongest postcondition (sp) . Thentcc sp denotes the set of all infinite output sequences that a given process can exhibit. The verification problemis 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 t imed ccp as well as for LTL. In particular, we shall prove that the following pro blems are decidable: (1) Thesp equivalencefor the so-calledlocally-independent ntcc fragment; unlike other fragments for which similar results have been pub lished, this fragment can specifyinfinite-state systems . (2) Verificationfor locally-independent processes and negation-free first-order formulae of thentcc LTL. (3) Implication for such formulae. (4) Satisfiabilityfor a first-order fragment of Manna and Pnueli's LTL. The purpose of the last result is to illustrate the appli cability of ccp to wellestablished formalisms for concurrency. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://www.brics.dk/~fvalenci/tcs.ps.gz |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
