Implementation of propositional temporal logics using BDDs

G.L.J.M. Janssen

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

96 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationTABLEAUX, automated reasoning with analytic tableaux and related methods : international conference, 1998, Oisterwijk, The Netherlands, May 5-8, 1998 : proceedings
EditorsH. Swart, de
Place of PublicationBerlin
Number of pages2
ISBN (Print)3-540-64406-7
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Implementation of propositional temporal logics using BDDs'. Together they form a unique fingerprint.

Cite this