This tutorial intends to convey the step-by-step process by which computer programs for model checking and satisfiability testing for temporal logics may be derived from the theory. The idea is to demonstrate that it is very well possible to implement such a program in an efficient way without sacrificing a correct-by-construction approach. The tutorial will be fully self-contained, only a general knowledge of programming and propositional logic is assumed.
|Title of host publication||TABLEAUX, automated reasoning with analytic tableaux and related methods : international conference, 1998, Oisterwijk, The Netherlands, May 5-8, 1998 : proceedings|
|Editors||H. Swart, de|
|Place of Publication||Berlin|
|Number of pages||2|
|Publication status||Published - 1998|
|Name||Lecture Notes in Computer Science|