Skip to main content
SpringerLink
Log in

Model Checking Propositional Deontic Temporal Logic via a μ-Calculus Characterization

  • Conference paper
Formal Methods: Foundations and Applications (SBMF 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7498))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bernardeschi, C., Fantechi, A., Gnesi, S.: Model checking fault tolerant systems. Softw. Test., Verif. Reliab. 12(4), 251–275 (2002)

    Article  Google Scholar 

  2. Biere, A.: μcke - Efficient μ-Calculus Model Checking. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 468–471. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  3. Castro, P.F.: Deontic Action Logics for the Specification and Analysis of Fault-Tolerance. PhD thesis, McMaster University, Department of Computing and Software (2009)

    Google Scholar 

  4. Castro, P.F., Maibaum, T.S.E.: A Tableaux System for Deontic Action Logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 34–48. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Castro, P.F., Maibaum, T.S.E.: Deontic action logic, atomic boolean algebra and fault-tolerance. Journal of Applied Logic 7(4), 441–466 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Coenen, J.: Formalisms for Program Reification and Fault Tolerance. PhD thesis, Tenische Universiteit Eindhoven (1994)

    Google Scholar 

  7. Cristian, F.: A rigorous approach to fault-tolerant programming. IEEE Trans. Software Eng. 11, 23–31 (1985)

    Article  Google Scholar 

  8. French, T., Mc Cabe-Dansted, J.C., Reynolds, M.: A Temporal Logic of Robustness. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 193–205. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Gärtner, F.: Specification for fault-tolerance: A comedy of failures. Technical report, Darmstadt University of Technology (1998)

    Google Scholar 

  10. Goguen, J.A., Burstall, R.M.: Institutions: Abstract model theory for specification and programming. Journal of the Association of Computing Machinery (1992)

    Google Scholar 

  11. Goguen, J.A., Rosu, G.: Institution morphisms. Formal Asp. Comput. 13(3-5), 274–307 (2002)

    Article  MATH  Google Scholar 

  12. Janowski, T.: On Bisimulation, Fault-Monotonicity and Provable Fault-tolerance. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 292–306. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  13. Lamport, L., Merz, S.: Specifying and Verifying Fault-Tolerant Systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 41–76. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  14. Laranjeira, L.A., Malek, M., Jenevein, R.M.: Nest: A nested-predicate scheme for fault tolerance. IEEE Trans. Computers 42, 1303–1324 (1993)

    Article  Google Scholar 

  15. Liu, Z., Joseph, M.: Specification and verification of fault-tolerance, timing, and scheduling. ACM Trans. Program. Lang. Syst. 21(1), 46–89 (1999)

    Article  Google Scholar 

  16. Lomuscio, A., Sergot, M.J.: A formalisation of violation, error recovery, and enforcement in the bit transmission problem. Journal of Applied Logic 2, 93–116 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  17. Magee, J., Maibaum, T.S.E.: Towards specification, modelling and analysis of fault tolerance in self managed systems. In: Proceeding of the 2006 International Workshop on Self-Adaptation and Self-Managing Systems (2006)

    Google Scholar 

  18. Schneider, F., Easterbrook, S.M., Callahan, J.R., Holzmann, G.J.: Validating requirements for fault tolerant systems using model checking. In: 3rd International Conference on Requirements Engineering, ICRE 1998 (1998)

    Google Scholar 

  19. Schneider, K.: Verification of Reactive Systems, Formal Methods and Algorithms. Springer (2004)

    Google Scholar 

  20. Yokogawa, T., Tsuchiya, T., Kikuno, T.: Automatic verification of fault tolerance using model checking. In: Pacific Rim International Symposium on Dependable Computing (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Facultad de Matemática, Astronomía y Física, Universidad Nacional de Córdoba, Córdoba, Argentina

    Araceli Acosta

  2. Departamento de Computación, FCEFQyN, Universidad Nacional de Río Cuarto, Río Cuarto, Argentina

    Cecilia Kilmurray, Pablo F. Castro & Nazareno M. Aguirre

  3. Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Argentina

    Pablo F. Castro & Nazareno M. Aguirre

Authors
  1. Araceli Acosta
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cecilia Kilmurray
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pablo F. Castro
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Nazareno M. Aguirre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Sistemas e Computacao, Universidade Federal de Campina Grande, Aprigio Veloso, 882, 58429 900, Campina Grande, PB, Brazil

    Rohit Gheyi

  2. Department of Computer Science, Stevens Institute of Technology, 07030, Hoboken, NJ, USA

    David Naumann

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Acosta, A., Kilmurray, C., Castro, P.F., Aguirre, N.M. (2012). Model Checking Propositional Deontic Temporal Logic via a μ-Calculus Characterization. In: Gheyi, R., Naumann, D. (eds) Formal Methods: Foundations and Applications. SBMF 2012. Lecture Notes in Computer Science, vol 7498. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33296-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33296-8_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33295-1

  • Online ISBN: 978-3-642-33296-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation