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 条
  • [21] SAT-based software certification
    Chaki, S
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 151 - 166
  • [22] An implementation of deterministic tree automata minimization
    Carrasco, Rafael C.
    Daciuk, Jan
    Forcada, Mikel L.
    [J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA, 2007, 4783 : 122 - +
  • [23] SAT-based Redundancy Removal
    Debnath, Krishanu
    Murgai, Rajeev
    Jain, Mayank
    Olson, Janet
    [J]. PROCEEDINGS OF THE 2018 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2018, : 315 - 318
  • [24] A SAT-Based Approach to MinSAT
    Ansotegui, Carlos
    Li, Chu Min
    Manya, Felip
    Zhu, Zhu
    [J]. ARTIFICIAL INTELLIGENCE RESEARCH AND DEVELOPMENT, 2012, 248 : 185 - +
  • [25] Efficient minimization of deterministic weak ω-automata
    Löding, C
    [J]. INFORMATION PROCESSING LETTERS, 2001, 79 (03) : 105 - 109
  • [26] A Split-Based Incremental Deterministic Automata Minimization Algorithm
    Garcia, Pedro
    Vazquez de Parga, Manuel
    Velasco, Jairo A.
    Lopez, Damian
    [J]. THEORY OF COMPUTING SYSTEMS, 2015, 57 (02) : 319 - 336
  • [27] A Split-Based Incremental Deterministic Automata Minimization Algorithm
    Pedro García
    Manuel Vázquez de Parga
    Jairo A. Velasco
    Damián López
    [J]. Theory of Computing Systems, 2015, 57 : 319 - 336
  • [28] Incremental SAT instance generation for SAT-based ATPG
    Tille, Daniel
    Drechsler, Rolf
    [J]. 2008 IEEE WORKSHOP ON DESIGN AND DIAGNOSTICS OF ELECTRONIC CIRCUITS AND SYSTEMS, PROCEEDINGS, 2008, : 68 - 73
  • [29] SAT-Based verification of LTL formulas
    Zhang, Wenhui
    [J]. FORMAL METHODS: APPLICATIONS AND TECHNOLOGY, 2007, 4346 : 277 - 292
  • [30] SAT-based cooperative planning: A proposal
    Benedetti, M
    Aiello, LC
    [J]. MECHANIZING MATHEMATICAL REASONING: ESSAYS IN HONOUR OF JORG H SIEKMANN ON THE OCCASION OF HIS 60TH BIRTHDAY, 2005, 2605 : 494 - 513
12345