Tableaux for Verification of Data-Centric Processes

Select |




Print


Bauer, Andreas; Baumgartner, Peter; Martin, Diller; Norrish, Michael

Bauer, Andreas; Baumgartner, Peter; Martin, Diller; Norrish, Michael


2013-09-16


Conference Material


Automated Reasoning with Analytic Tableaux and Related Methods


Nancy, France


28-43


Current approaches to analyzing dynamic systems are mostly grounded in propositional (temporal) logics. As a consequence, they often lack expressivity for modelling rich data structures and reasoning about them in the course of a computation. To address this problem, we propose a rich modelling framework based on first-order logic over background theories (arithmetics, lists, records, etc) and state transition systems over corresponding interpretations. On the reasoning side, we introduce a tableau calculus for bounded model checking of properties expressed in a certain fragment of CTL* over that first-order logic. To overcome to some degree the limits of bounded model checking, we incorporate k-induction for proving safety properties.


Springer Verlag


Model Checking, first-order logic, business processes


https://doi.org/10.1007/978-3-642-40537-2_5


http://tableaux13.loria.fr


Copyright Springer Verlag http://www.springer.de/comp/lncs/index.html


nicta:6988


Bauer, Andreas; Baumgartner, Peter; Martin, Diller; Norrish, Michael. Tableaux for Verification of Data-Centric Processes. In: Didier Galmiche and Dominique Larchey-Wendling Editor, editor/s. Automated Reasoning with Analytic Tableaux and Related Methods; Nancy, France. Springer Verlag; 2013-09-16. 28-43. https://doi.org/10.1007/978-3-642-40537-2_5



Loading citation data...

Citation counts
(Requires subscription to view)