Springer Nature is making SARS-CoV-2 and COVID-19 research free. View research | View latest news | Sign up for updates

Minimal refinements of specifications in modal and temporal logics

  • 43 Accesses

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

References

  1. AL91

    Abadi M, Lamport L(1991) The existence of refinement mappings. Theor Comput Sci 82(2):253–284

  2. BCM+90

    Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ(1990) Symbolic model checking: 1020 states and beyond. In: Proceedings of the fifth annual IEEE symposium on logic in computer science, IEEE Computer Society Press, Washington pp 1–33

  3. BdRV01

    Blackburn P, de Rijke M, Venema Y(2001) Modal logic, vol 53 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge

  4. BEF93

    van Benthem J, van Eijck J, Frolova A(1993) Changing preferences. Technical Report CS-93-10, Centre for Mathematics and Computer Science, Amsterdam

  5. BFG+91

    Bouajjani A, Fernandez JC, Graf S, Rodriguez C, Sifakis J(1991) Safety for branching time semantics. In: Proceedings of the 18th international colloquium on automata, languages and programming, ICALP’91, vol 510 of LNCS, Madrid, Spain. Springer, Berlin Heidelberg Newyork, pp 76–92

  6. BMP97

    Bezzazi H, Makinson D, Pérez RP(1997) Beyond rational monotony: Some strong non-horn rules for nonmonotonic inference relations. J Logic Comput 7(5):605–631

  7. CE81

    Clarke EM, Emerson EA(1981) The design and synthesis of synchronization skeletons using temporal logic. In Workshop on Logics of Programs, vol 131 of LNCS, Yorktown Heights.Springer Berlin Heidelberg Newyork, pp 52–72

  8. CES86

    Clarke EM, Emerson EA, Sistla AP(1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263

  9. CGL96

    Clarke EM, Grumberg O, Long D(1996) Model checking. Nato ASI Series F, vol 152. Springer,Berlin Heidelberg Newyork Marktoberdorf summer school

  10. Che80

    Chellas BF(1980) Modal Logic: An introduction. Cambridge University Press, Cambridge

  11. Dal88

    Dalal M(1988) Investigations into a theory of knowledge base revision: Preliminary report. In: Proceedings of the 7th national conference on artificial intelligence. St. Paul, Minnesota, pp. 475–479

  12. dR95

    de Rijke M(1995) Modal model theory. Technical Report CS–R9517, CWI, Amsterdam (1995)

  13. GL94

    Grumberg O, Long DE(1994) Model checking and modular verification. ACM Tran Program Lang Syst 16(3):843–871

  14. Gor03

    Gorogiannis N(2003) Computing minimal changes of models of systems. PhD Thesis, School of Computer Science, University of Birmingham,

  15. GR02

    Gorogiannis N, Ryan MD(2002) Requirements, specifications and minimal refinement. In: 9th workshop on logic, language, information and computation, vol 67 of electronic notes in theoretical computer science. Elsevier, Amsterdam

  16. Gro88

    Grove A(1988) Two modelings for theory change. J Philos Logic 17:157–170

  17. Hal95

    Halpern JY(1995) The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. Artificial Intelligence 75(2):361–372

  18. HKR97

    Henzinger TA, Kupferman O, Rajamani SK(1997) Fair simulation. In: Proceedings of the 9th international conference on concurrency theory (CONCUR), vol 1243 of Lecture Notes in Computer Science. Springer,Berlin Heidelberg Newyork, pp 273–287

  19. HM85

    Hennessy M, Milner R(1985) Algebraic laws for nondeterminism and concurrency. J ACM 32(1):137–161

  20. Hol95

    Hollenberg M(1995) Hennessy-Milner classes and process algebra. In: Ponse A, de Rijke M, Venema Y (eds), Modal Logic and Process Algebra. pp 187–216. CSLI Publications, 1995.

  21. HR04

    Huth MR, Ryan MD(2004) Logic in Computer Science: Modelling and reasoning about systems, 2nd edn. Cambridge University Press, Cambridge

  22. KGG99

    Katz S, Grumberg O, Geist D(1999) Have I written enough properties? - a method of comparison between specification and implementation. In: Conference on correct hardware design and verification methods, pp 280–297

  23. KLM90

    Kraus S, Lehmann D, Magidor M(1990) Nonmonotonic reasoning, preferential models and cumulative logics. Artif Intell 44:167–207

  24. KM89

    Katsuno H, Mendelzon AO(1989) A unified view of propositional knowledge base updates. In: Proceedings of the eleventh international joint conference on artificial intelligence, Detroit pp 1413–1419

  25. KM91

    Katsuno H, Mendelzon AO(1991) Propositional knowledge base revision and minimal change. Artificial Intelligence 52:263–294

  26. KM92

    Katsuno H, Mendelzon AO(1992) On the difference between updating a knowledge base and revising it. In: Gärdenfors P, (ed) Belief revision, Cambridge Computer Tracts. Cambridge University Press, Cambridge, pp 183–203

  27. Mai00

    Maidl M(2000) The common fragment of CTL and LTL. In: Proceedings of the 41th annual symposium on foundations of computer science, pp 643–652

  28. McM93

    McMillan KL(1993) Symbolic model checking. Kluwer, Dordrecht

  29. Mey91

    van der Meyden R(1991) A clausal logic for deontic action specification. In: Proceedings of the international logic programming symposium, MIT Press, San Diego, pp 221–238

  30. Mil71

    Milner R(1971) An algebraic definition of simulation between programs. In: Proceedings of the 2nd international joint conference on artificial intelligence, London, pp 481–489

  31. NDG+

    North S,Dobkin D, Gansner E, Koutsofios E, Vo K, Woodhull G Graphviz, A suite of tools for visualizing graphs. Can be obtained from http://www.graphviz.org

  32. PMT02

    Peng H, Mokhtari Y, Tahar S(2002) Environment synthesis for compositional model checking. In: Proceedings of the IEEE international conference on computer design. IEEE Computer Society Press, pp 70–75

Download references

Author information

Correspondence to Mark Ryan.

Additional information

A. Sernadas

Rights and permissions

Reprints and Permissions

About this article

Cite this article

Gorogiannis, N., Ryan, M. Minimal refinements of specifications in modal and temporal logics. Form Asp Comp 19, 417–444 (2007). https://doi.org/10.1007/s00165-007-0040-9

Download citation

Keywords

  • Model Check
  • Modal Logic
  • Temporal Logic
  • Critical Section
  • Kripke Model