A model checker for linear time temporal logic

M. Fisher

doi:10.1007/BF01212306

A model checker for linear time temporal logic

M. Fisher

Autonomy and Verification

Research output: Contribution to journal › Article › peer-review

Abstract

This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.

Original language	English
Pages (from-to)	299 - 319
Number of pages	21
Journal	Formal Aspects of Computing
Volume	4
Issue number	3
DOIs	https://doi.org/10.1007/BF01212306
Publication status	Published - 1 May 1992

Keywords

Model checking
Program verification
Temporal logic

Access to Document

10.1007/BF01212306

Cite this

@article{17ebc7a75d1645e0b1c0df4ee238e841,

title = "A model checker for linear time temporal logic",

abstract = "This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.",

keywords = "Model checking, Program verification, Temporal logic",

author = "M. Fisher",

year = "1992",

month = may,

day = "1",

doi = "10.1007/BF01212306",

language = "English",

volume = "4",

pages = "299 -- 319",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery",

number = "3",

}

TY - JOUR

T1 - A model checker for linear time temporal logic

AU - Fisher, M.

PY - 1992/5/1

Y1 - 1992/5/1

N2 - This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.

AB - This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.

KW - Model checking

KW - Program verification

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?eid=2-s2.0-33745567012&partnerID=MN8TOARS

U2 - 10.1007/BF01212306

DO - 10.1007/BF01212306

M3 - Article

SN - 0934-5043

VL - 4

SP - 299

EP - 319

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 3

ER -

A model checker for linear time temporal logic

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this