A new unfolding approach to LTL model checking

Javier Esparza, Keijo Heljanko

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

20 Scopus citations

Abstract

A new unfolding approach to LTL model checking is presented, in which the model checking problem can be solved by direct inspection of a certain finite prefix. The techniques presented so far required to run an elaborate algorithm on the prefix.

Original languageEnglish
Title of host publicationAutomata, Languages and Programming - 27th International Colloquium, ICALP 2000, Proceedings
EditorsUgo Montanari, Jose D. P. Rolim, Emo Welzl
PublisherSpringer Verlag
Pages475-486
Number of pages12
ISBN (Print)9783540450221
DOIs
StatePublished - 2000
Event27th International Colloquium on Automata, Languages and Programming, ICALP 2000 - Geneva, Switzerland
Duration: 9 Jul 200015 Jul 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1853
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference27th International Colloquium on Automata, Languages and Programming, ICALP 2000
Country/TerritorySwitzerland
CityGeneva
Period9/07/0015/07/00

Fingerprint

Dive into the research topics of 'A new unfolding approach to LTL model checking'. Together they form a unique fingerprint.

Cite this