Branching-Time Model Checking Gap-Order Constraint Systems

• Autorzy: Mayr R. , Totzke P.

Identyfikatory

DOI

10.3233/FI-2016-1317

• Języki publikacji: EN

Abstrakty

EN

We consider the model checking problem for Gap-order Constraint Systems (GCS) w.r.t. the branching-time temporal logic CTL, and in particular its fragments EG and EF. GCS are nondeterministic infinitely branching processes described by evolutions of integer-valued variables, subject to Presburger constraints of the form x−y ≥ k, where x and y are variables or constants and k ∈ N is a non-negative constant. We show that EG model checking is undecidable for GCS, while EF is decidable. In particular, this implies the decidability of strong and weak bisimulation equivalence between GCS and finite-state systems.

Słowa kluczowe

EN

mathematical models; problem solving; branching processes; integers; variables; computational complexity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2016
• Tom: Vol. 143, nr 3/4
• Strony: 339--353
• Opis fizyczny: Bibliogr 19 poz.

Twórcy

autor

Mayr R.

• University of Edinburgh, UK

autor

Totzke P.

• University of Warwick, UK

Bibliografia

• [1] Minsky ML. Computation: finite and infinite machines. Upper Saddle River, NJ, USA: Prentice-Hall, Inc.; 1967. ISBN:0-13-165563-9.
• [2] Mayr EW. An Algorithm for the General Petri Net Reachability Problem. SIAMJ Comput. 1984;13(3):441–460. DOI:10.1137/0213029.
• [3] Revesz PZ. A Closed-Form Evaluation for Datalog Queries with Integer (Gap)-Order Constraints. TCS. 1993;116(1&2):117–149. DOI:10.1016/0304-3975(93)90222-F.
• [4] Fribourg L, Richardson J. Symbolic Verification with Gap-Order Constraints. In: LOPSTR. vol. 1207 of LNCS; 1996. p. 20–37. ISBN:3-540-62718-9.
• [5] Bozzelli L. Strong Termination for Gap-Order Constraint Abstractions of Counter Systems. In: LATA. vol.7183 of LNCS; 2012. p. 155–168. DOI:10.1007/978-3-642-28332-1 14.
• [6] Bozzelli L, Pinchinat S. Verification of Gap-Order Constraint Abstractions of Counter Systems. In: VMCAI. vol. 7148 of LNCS. Springer; 2012. p. 88–103. DOI:10.1007/978-3-642-27940-9 7.
• [7] Abdulla PA, Delzanno G. Constrained Multiset Rewriting. In: Proc. AVIS’06, 5th int. workshop on Automated Verification of InfiniteState Systems; 2006.
• [8] Cerans K. Deciding Properties of Integral Relational Automata. In: ICALP. vol. 820 of LNCS; 1994. p. 35–46. DOI:10.1007/3-540-58201-0 56.
• [9] Ben-Amram AM. Size-Change Termination, Monotonicity Constraints and Ranking Functions. In: Bouajjani A, Maler O, editors. Computer Aided Verification. vol. 5643 of LNCS. Springer; 2009. p. 109–123. DOI:10.1007/978-3-642-02658-4 12.
• [10] Demri S, D’Souza D. An automata-theoretic approach to constraint LTL. Inf Comput. 2007;205(3):380–415. DOI:10.1016/j.ic.2006.09.006.
• [11] Esparza J. Decidability of Model Checking for Infinite-State Concurrent Systems. Acta Informatica. 1997;34:85–107. DOI:10.1007/s002360050074.
• [12] Cook S, Soltys M. Boolean programs and quantified propositional proof systems. Bulletin of the Section of Logic. 1999.
• [13] Ball T, Rajamani SK. Boolean Programs: A Model and Process for Software Analysis. Microsoft Research; 2000. MSR-TR-2000-14.
• [14] Figueira D, Figueira S, Schmitz S, Schnoebelen P. Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma. In: LICS; 2011. p. 269–278. DOI:10.1109/LICS.2011.39.
• [15] Park D. Concurrency and automata on infinite sequences. In: TCS. vol. 104 of LNCS; 1981. p. 167–183. DOI:10.1007/BFb0017309.
• [16] Milner R. Communication and concurrency. PHI Series in computer science. Prentice Hall; 1989. ISBN:0131149849.
• [17] Glabbeek RJv. The Linear Time – Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes. In: Bergstra JA, Ponse A, Smolka SA, editors. Handbook of Process Algebra. Elsevier; 2001. p. 3–99. DOI:10.1007/BFb0039066.
• [18] Kučera A, Jančar P. Equivalence-checking on infinite-state systems: Techniques and results. TPLP. 2006;6(3):227–264. DOI:10.1017/S147106840600265.
• [19] Jančar P, Kučera A, Mayr R. Deciding Bisimulation-Like Equivalences with Finite-State Processes. In: ICALP. vol. 1443 of LNCS; 1998. p. 200–211.