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 条
  • [31] SAT-Based verification of LTL formulas
    Zhang, Wenhui
    [J]. FORMAL METHODS: APPLICATIONS AND TECHNOLOGY, 2007, 4346 : 277 - 292
  • [32] Iterative abstraction using SAT-based BMC with proof analysis
    Gupta, A
    Ganai, M
    Yang, Z
    Ashar, P
    [J]. ICCAD-2003: IEEE/ACM DIGEST OF TECHNICAL PAPERS, 2003, : 416 - 423
  • [33] An analysis of SAT-based model checking techniques in an industrial environment
    Amla, N
    Du, XQ
    Kuehlmann, A
    Kurshan, RP
    McMillan, KL
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2005, 3725 : 254 - 268
  • [34] A SAT-based algorithm for context matching
    Bouquet, P
    Magnini, B
    Serafini, L
    Zanobini, S
    [J]. MODELING AND USING CONTEXT, PROCEEDINGS, 2003, 2680 : 66 - 79
  • [35] The SAT-based Approach to Separation Logic
    Alessandro Armando
    Claudio Castellini
    Enrico Giunchiglia
    Marco Maratea
    [J]. Journal of Automated Reasoning, 2005, 35 : 237 - 263
  • [36] SAT-based model-checking for security protocols analysis
    Armando, Alessandro
    Compagna, Luca
    [J]. INTERNATIONAL JOURNAL OF INFORMATION SECURITY, 2008, 7 (01) : 3 - 32
  • [37] SAT-Based ATL Satisfiability Checking
    Kacprzak, Magdalena
    Niewiadomski, Artur
    Penczek, Wojciech
    [J]. KR2020: PROCEEDINGS OF THE 17TH INTERNATIONAL CONFERENCE ON PRINCIPLES OF KNOWLEDGE REPRESENTATION AND REASONING, 2020, : 539 - 549
  • [38] The SAT-based approach to separation logic
    Armando, Alessandro
    Castellini, Claudio
    Giunchiglia, Enrico
    Maratea, Marco
    [J]. JOURNAL OF AUTOMATED REASONING, 2005, 35 (1-3) : 237 - 263
  • [39] SAT-based summarization for boolean programs
    Basler, Gerard
    Kroening, Daniel
    Weissenbacher, Georg
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2007, 4595 : 131 - +
  • [40] Interpolation and SAT-based model checking
    McMillan, KL
    [J]. COMPUTER AIDED VERIFICATION, 2003, 2725 : 1 - 13
12345