Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)

Sylvain Kerjean; Froduald Kabanza; Richard St-Denis; Sylvie Thiébaux

doi:10.1016/j.entcs.2005.07.028

Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)

Sylvain Kerjean^*
, Froduald Kabanza
, Richard St-Denis
, Sylvie Thiébaux

^*Corresponding author for this work

Research output: Contribution to journal › Conference article › peer-review

8 Citations (Scopus)

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 checking: verification, plan synthesis as well as heuristic guidance of AI planning, and controller synthesis. We include results from benchmarks obtained from preparatory experiments with model checking using a family of LTL2Büchi translators and formula progression.

Original language	English
Pages (from-to)	91-104
Number of pages	14
Journal	Electronic Notes in Theoretical Computer Science
Volume	149
Issue number	2
DOIs	https://doi.org/10.1016/j.entcs.2005.07.028
Publication status	Published - 14 Feb 2006
Event	Proceedings of the Third Workshop on MOdel Checking and Artifical Intelligence (MoChArt 2005) - Duration: 16 Mar 2005 → 19 Mar 2005

Access to Document

10.1016/j.entcs.2005.07.028

Cite this

@article{0725533dfe6846b8b946d7214667054e,

title = "Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)",

abstract = "In this paper, we present alternative means of handling invariances in reachability testing, either by formula progression or compilation into B{\"u}chi automata. These alternatives are presented in connection with three different applications of model checking: verification, plan synthesis as well as heuristic guidance of AI planning, and controller synthesis. We include results from benchmarks obtained from preparatory experiments with model checking using a family of LTL2B{\"u}chi translators and formula progression.",

keywords = "Formula progression, LTL2B{\"u}chi translators, Model checking, Synthesis, Verification",

author = "Sylvain Kerjean and Froduald Kabanza and Richard St-Denis and Sylvie Thi{\'e}baux",

year = "2006",

month = feb,

day = "14",

doi = "10.1016/j.entcs.2005.07.028",

language = "English",

volume = "149",

pages = "91--104",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

number = "2",

note = "Proceedings of the Third Workshop on MOdel Checking and Artifical Intelligence (MoChArt 2005) ; Conference date: 16-03-2005 Through 19-03-2005",

}

TY - JOUR

T1 - Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)

AU - Kerjean, Sylvain

AU - Kabanza, Froduald

AU - St-Denis, Richard

AU - Thiébaux, Sylvie

PY - 2006/2/14

Y1 - 2006/2/14

N2 - 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 checking: verification, plan synthesis as well as heuristic guidance of AI planning, and controller synthesis. We include results from benchmarks obtained from preparatory experiments with model checking using a family of LTL2Büchi translators and formula progression.

AB - 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 checking: verification, plan synthesis as well as heuristic guidance of AI planning, and controller synthesis. We include results from benchmarks obtained from preparatory experiments with model checking using a family of LTL2Büchi translators and formula progression.

KW - Formula progression

KW - LTL2Büchi translators

KW - Model checking

KW - Synthesis

KW - Verification

UR - https://www.scopus.com/pages/publications/31644433450

U2 - 10.1016/j.entcs.2005.07.028

DO - 10.1016/j.entcs.2005.07.028

M3 - Conference article

SN - 1571-0661

VL - 149

SP - 91

EP - 104

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 2

T2 - Proceedings of the Third Workshop on MOdel Checking and Artifical Intelligence (MoChArt 2005)

Y2 - 16 March 2005 through 19 March 2005

ER -

Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)

Abstract

Access to Document

Other files and links

Fingerprint

Cite this