SAT-Based Minimization of Deterministic ω-Automata

被引：5
|
作者：
Baarir, Souheib [1 ]
Duret-Lutz, Alexandre [1 ]
机构：
[1] EPITA, LRDE, Le Kremlin Bicetre, France
来源：
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, (LPAR-20 2015) | 2015年 / 9450卷
关键词：
D O I：
10.1007/978-3-662-48899-7_6
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We describe a tool that inputs a deterministic omega-automaton with any acceptance condition, and synthesizes an equivalent omega-automaton with another arbitrary acceptance condition and a given number of states, if such an automaton exists. This tool, that relies on a SAT-based encoding of the problem, can be used to provide minimal omega-automata equivalent to given properties, for different acceptance conditions.
引用
收藏
页码：79 / 87
页数：9
相关论文
共 50 条
  • [1] SAT-based analysis of cellular automata
    D'Antonio, M
    Delzanno, G
    [J]. CELLULAR AUTOMATA, PROCEEDINGS, 2004, 3305 : 745 - 754
  • [2] SAT-Based algorithms for logic minimization
    Sapra, S
    Theobald, M
    Clarke, E
    [J]. 21ST INTERNATIONAL CONFERENCE ON COMPUTER DESIGN, PROCEEDINGS, 2003, : 510 - 517
  • [3] Core Minimization in SAT-based Abstraction
    Belov, Anton
    Chen, Huan
    Mishchenko, Alan
    Marques-Silva, Joao
    [J]. DESIGN, AUTOMATION & TEST IN EUROPE, 2013, : 1411 - 1416
  • [4] 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
  • [5] SAT-based Unbounded Model Checking of Timed Automata
    Penczek, Wojciech
    Szreter, Maciej
    [J]. FUNDAMENTA INFORMATICAE, 2008, 85 (1-4) : 425 - 440
  • [6] 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
  • [7] Improvements in SAT-based reachability analysis for timed automata
    Zbrzezny, A
    [J]. FUNDAMENTA INFORMATICAE, 2004, 60 (1-4) : 417 - 434
  • [8] SAT-Based State Encoding for Peak Current Minimization
    Lee, Yongho
    Choi, Kiyoung
    Kim, Taewhan
    [J]. 2009 INTERNATIONAL SOC DESIGN CONFERENCE (ISOCC 2009), 2009, : 432 - 435
  • [9] A Dynamic Expansion Order Algorithm for the SAT-based Minimization
    Lin, Chia-Chun
    Tam, Kit Seng
    Ko, Chana-Cheng
    Yen, Hsin-Ping
    Wei, Shenz-Hsiu
    Chen, Yung-Chih
    Wang, Chun-Yao
    [J]. 2020 IEEE 33RD INTERNATIONAL SYSTEM-ON-CHIP CONFERENCE (SOCC), 2020, : 271 - 276
  • [10] SAT-Based reachability checking for timed automata with discrete data
    Zbrzezny, Andrzej
    Polrola, Agata
    [J]. FUNDAMENTA INFORMATICAE, 2007, 79 (3-4) : 579 - 593
12345