Analyzing LTL model checking techniques for plan synthesis and controller synthesis
Date
2006
Authors
Kerjean, Sylvain
Kabanza, Froduald
St-Denis, Richard
Thiebaux, Sylvie
Journal Title
Journal ISSN
Volume Title
Publisher
Elsevier
Abstract
In this paper, we present alternative means of handling invariances in reachability testing, either by formula progression or compilation into Büchi automata. These alternatives are presented in connection with three different applications of model check
Description
Keywords
Keywords: Benchmarking; Mathematical models; Program translators; Formula progression; Model checking; Synthesis; Verification; Control equipment Formula progression; LTL2Bchi translators; Model checking; Synthesis; Verification
Citation
Collections
Source
Electronic Notes in Theoretical Computer Science
Type
Journal article
Book Title
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description