Modal Logic as a Design Notation

C. Areces, M. Felder, D. Hirsch, and D. Yankelevich. Modal Logic as a Design Notation. In Proceedings of the 1st KIT125 Workshop, pp. 93–108, Como, Italy, 1997.

Download

[pdf] 

Abstract

A notation to describe software system designs is given together with the means to verify properties over them. Design graphs are considered as models of an extended modal logic. The procedure to derive the modal model associated with a design, the algorithm to check properties over a model, the method to define new relations and the method fo model fitration are presented. These methods are introduced using the classic example of KWIC (Key Word in Context) and further tested on two different design systems to show their usefulness and generality. The logic proposed is called KPI (a poly-modal logic with inverse operators) and will be used as a property specification language verified through an algorithm of model checking. The methods proposed are effective and simple to implement.

BibTeX

@InProceedings{Areces1997,
  author =       "C. Areces and M. Felder and D. Hirsch and D.
                 Yankelevich",
  booktitle =    "Proceedings of the 1st KIT125 Workshop",
  title =        "Modal Logic as a Design Notation",
  year =         "1997",
  address =      "Como, Italy",
  pages =        "93--108",
  abstract =     "A notation to describe software system designs is
                 given together with the means to verify properties over
                 them. Design graphs are considered as models of an
                 extended modal logic. The procedure to derive the modal
                 model associated with a design, the algorithm to check
                 properties over a model, the method to define new
                 relations and the method fo model fitration are
                 presented. These methods are introduced using the
                 classic example of KWIC (Key Word in Context) and
                 further tested on two different design systems to show
                 their usefulness and generality. The logic proposed is
                 called KPI (a poly-modal logic with inverse operators)
                 and will be used as a property specification language
                 verified through an algorithm of model checking. The
                 methods proposed are effective and simple to
                 implement.",
}