Model Checking Propositional Deontic Temporal Logic via Mu-Calculus Characterization

ARACELI ACOSTA; CECILIA KILMURRAY; PABLO F. CASTRO; NAZARENO AGUIRRE

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlin; Año: 2012 vol. 7498 p. 3 - 18

0302-9743

In this paper, we present a characterization of a propositional deontic temporal logic into μ-calculus. This logic has been proposed to specify and reason about fault tolerant systems, and even though is known to be decidable, no tool realizing its corresponding decision procedure has been developed. A main motivation for our work is enabling for the use of model checking, for analyzing specifications in this deontic temporal logic. We present the technical details involved in the characterization, and prove that the model checking problem on the deontic temporal logic is correctly reduced to μ-calculus model checking. We also show that counterexamples are preserved, which is crucial for our model checking purposes. Finally, we illustrate our approach via a case study, including the verification of some properties using a μ-calculus model checker.