SAT-based analysis of cellular automata

被引：0
|
作者：
D'Antonio, M [1 ]
Delzanno, G [1 ]
机构：
[1] Univ Genoa, Dipartimento Informat & Sci Informaz, I-16146 Genoa, Italy
来源：
CELLULAR AUTOMATA, PROCEEDINGS | 2004年 / 3305卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In the last decade there has been a dramatic speed-up for algorithms solving the Satisfiability (SAT) problem for propositional formulas, a well known NP-complete problem. In this paper we will investigate the applicability of modern SAT solvers to the qualitative analysis of Cellular Automata. For this purpose we have defined an encoding of the evolution of Cellular Automata into formulas in propositional logic. The resulting formula can be used to test forward and inverse reachability problems for the original Cellular Automata in a modular way. In the paper we will report on experimental results obtained by applying the SAT-solver zChaff to reachability problems for classical examples of Cellular Automata like the Firing Squad Synchronization Problem.
引用
收藏
页码：745 / 754
页数：10
相关论文
共 50 条
  • [1] Improvements in SAT-based reachability analysis for timed automata
    Zbrzezny, A
    [J]. FUNDAMENTA INFORMATICAE, 2004, 60 (1-4) : 417 - 434
  • [2] SAT-Based Minimization of Deterministic ω-Automata
    Baarir, Souheib
    Duret-Lutz, Alexandre
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, (LPAR-20 2015), 2015, 9450 : 79 - 87
  • [3] Sat-based model checking for region automata
    Yu, Fang
    Wang, Bow-Yaw
    [J]. INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2006, 17 (04) : 775 - 795
  • [4] SAT-based Unbounded Model Checking of Timed Automata
    Penczek, Wojciech
    Szreter, Maciej
    [J]. FUNDAMENTA INFORMATICAE, 2008, 85 (1-4) : 425 - 440
  • [5] SAT-based unbounded model checking of timed automata
    Penczek, Wojciech
    Szreter, Maciej
    [J]. SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2007, : 236 - 237
  • [6] SAT-Based reachability checking for timed automata with discrete data
    Zbrzezny, Andrzej
    Polrola, Agata
    [J]. FUNDAMENTA INFORMATICAE, 2007, 79 (3-4) : 579 - 593
  • [7] SAF: SAT-Based Attractor Finder in Asynchronous Automata Networks
    Soh, Takehide
    Magnin, Morgan
    Le Berre, Daniel
    Banbara, Mutsunori
    Tamura, Naoyuki
    [J]. COMPUTATIONAL METHODS IN SYSTEMS BIOLOGY, CMSB 2023, 2023, 14137 : 175 - 183
  • [8] SAT-Based Automata Construction for LTL over Finite Traces
    Shi, Yingying
    Xiao, Shengping
    Li, Jianwen
    Guo, Jian
    Pu, Geguang
    [J]. 2020 27TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC 2020), 2020, : 1 - 10
  • [9] SAT-based reachability checking for timed automata with diagonal constraints
    Zbrzezny, A
    [J]. FUNDAMENTA INFORMATICAE, 2005, 67 (1-3) : 303 - 322
  • [10] SAT-based Analysis of Sensitisable Paths
    Sauer, Matthias
    Czutro, Alexander
    Schubert, Tobias
    Hillebrecht, Stefan
    Polian, Ilia
    Becker, Bernd
    [J]. 2011 IEEE 14TH INTERNATIONAL SYMPOSIUM ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS (DDECS), 2011, : 93 - 98
12345