On Identification of Input/Output Extended Automata with Finite Bisimilar Quotients

被引：1
|
作者：
Zhou, Changyan [1 ]
Kumar, Ratnesh [2 ]
机构：
[1] Magnatech LLC, E Granby, CT 06026 USA
[2] Iowa State Univ, Dept Elect & Comp Engn, Ames, IA 50011 USA
来源：
2009 AMERICAN CONTROL CONFERENCE, VOLS 1-9 | 2009年
基金：
美国国家科学基金会;
关键词：
Extended automata; symbolic transition systems; formal verification; bisimulation equivalence; software modeling; software abstraction; software verification; VERIFICATION; ABSTRACTIONS;
D O I：
10.1109/ACC.2009.5160198
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We study the problem of finding a finite bisimilar abstraction for a class of reactive untimed infinite-state systems, modeled as input-output extended finite automata (I/O-EFA). We identify a lower bound abstraction (that is coarser than any finite bisimilar abstraction), and present an iterative refinement algorithm whose termination guarantees the existence of a finite bisimilar abstraction. The termination condition is weaker than the one given in [15] for the existence of a finite bisimilar quotient, and thus, the paper identifies a larger class of I/O-EFAs possessing a finite bisimilar abstraction (than that given in [15]).
引用
收藏
页码：5653 / +
页数：3
相关论文
共 50 条
  • [21] OUTPUT STRUCTURE OF CERTAIN FINITE AUTOMATA
    JOHNSEN, VB
    INFORMATION AND CONTROL, 1974, 25 (03): : 195 - 205
  • [22] Fuzzy multiset finite automata with output
    Pavel Martinek
    Soft Computing, 2022, 26 : 13205 - 13217
  • [23] Extended symbolic finite automata and transducers
    D'Antoni, Loris
    Veanes, Margus
    FORMAL METHODS IN SYSTEM DESIGN, 2015, 47 (01) : 93 - 119
  • [24] Extended finite automata and word problems
    Corson, JM
    INTERNATIONAL JOURNAL OF ALGEBRA AND COMPUTATION, 2005, 15 (03) : 455 - 466
  • [25] Extended symbolic finite automata and transducers
    Loris D’Antoni
    Margus Veanes
    Formal Methods in System Design, 2015, 47 : 93 - 119
  • [26] Extended finite automata over groups
    Mitrana, V
    Stiebe, R
    DISCRETE APPLIED MATHEMATICS, 2001, 108 (03) : 287 - 300
  • [27] Performance of bidimensional location quotients for constructing input–output tables
    Pereira-López X.
    Sánchez-Chóez N.G.
    Fernández-Fernández M.
    Journal of Economic Structures, 10 (1)
  • [28] Product-forms for Probabilistic Input/Output Automata
    Cavallin, Filippo
    Marin, Andrea
    Rossi, Sabina
    2016 IEEE 24TH INTERNATIONAL SYMPOSIUM ON MODELING, ANALYSIS AND SIMULATION OF COMPUTER AND TELECOMMUNICATION SYSTEMS (MASCOTS), 2016, : 361 - 366
  • [29] Hybrid Input Output Automata for Composable Conveyor Systems
    Mitra, Sayan
    Sastry, Shivakumar
    2009 IEEE INTERNATIONAL CONFERENCE ON AUTOMATION SCIENCE AND ENGINEERING, 2009, : 29 - 29
  • [30] Brief Announcement: Probabilistic Dynamic Input/Output Automata
    Civit, Pierre
    Potop-Butucaru, Maria
    PROCEEDINGS OF THE 2022 ACM SYMPOSIUM ON PRINCIPLES OF DISTRIBUTED COMPUTING, PODC 2022, 2022, : 378 - 380
12345