Model checking using automata theory

被引：0
|
作者：
Peled, D [1 ]
机构：
[1] Bell Labs, Murray Hill, NJ 07974 USA
来源：
VERIFICATION OF DIGITAL AND HYBRID SYSTEM | 2000年 / 170卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
In this chapter, we describe the theory of LTL model checking using omega-automata theory. The relation between model checking algorithms and automata theory allows applying various known results about automata to the automatic verification of programs.
引用
收藏
页码：55 / 79
页数：5
相关论文
共 50 条
  • [1] Model Checking Using Generalized Testing Automata
    Ben Salem, Ala-Eddine
    Duret-Lutz, Alexandre
    Kordon, Fabrice
    [J]. TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY VI, 2012, 7400 : 94 - 122
  • [2] Linear-time model checking: Automata theory in practice
    Vardi, Moshe Y.
    [J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA, 2007, 4783 : 5 - 10
  • [3] Model Checking Coordination of CPS Using Timed Automata
    Jiang, Kaiqiang
    Guan, Chunlin
    Wang, Jiahui
    Du, Dehui
    [J]. 2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2018, : 258 - 263
  • [4] REGULAR AUTOMATA AND MODEL CHECKING
    HABASINSKI, Z
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1988, 299 : 231 - 243
  • [5] Model Checking Cancer Automata
    Bowles, Juliana K. F.
    Silvina, Agastya
    [J]. 2016 3RD IEEE EMBS INTERNATIONAL CONFERENCE ON BIOMEDICAL AND HEALTH INFORMATICS, 2016, : 376 - 379
  • [6] Model Checking Temporal Logic Formulas Using Sticker Automata
    Zhu, Weijun
    Feng, Changwei
    Wu, Huanmei
    [J]. BIOMED RESEARCH INTERNATIONAL, 2017, 2017
  • [7] Model checking timed automata with priorities using DBM subtraction
    David, Alexandre
    Hakansson, John
    Larsen, Kim G.
    Pettersson, Paul
    [J]. FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2006, 4202 : 128 - 142
  • [8] Model checking for probabilistic timed automata
    Norman, Gethin
    Parker, David
    Sproston, Jeremy
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2013, 43 (02) : 164 - 190
  • [9] Model Checking for a Class of Weighted Automata
    Peter Buchholz
    Peter Kemper
    [J]. Discrete Event Dynamic Systems, 2010, 20 : 103 - 137
  • [10] Model checking for probabilistic timed automata
    Gethin Norman
    David Parker
    Jeremy Sproston
    [J]. Formal Methods in System Design, 2013, 43 : 164 - 190
12345