Recasting constraint automata into Buchi automata

被引:0
|
作者
Izadi, Mohammad [1 ]
Bonsangue, Marcello A. [1 ]
机构
[1] Leiden Univ, LIACS, NL-2300 RA Leiden, Netherlands
关键词
D O I
暂无
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Constraint automata have been proposed as the operational semantics of Reo, a glue-code language for the exogenous composition and orchestration of components in a software system. In this paper we recast the theory of constraint automata into that of Buchi automata on infinite strings of records. We use records to express simultaneity constraints of I/O operations and show that every constraint automaton can be expressed as a, Buchi automaton on an appropriate alphabet of records. Further, we give examples of component compositions that are expressible as Buchi automata but not as constraint automata. Finally, we show that the join composition operator for constraint automata and its counterpart for Buchi automata of records can be expressed as two basic operations on Buchi automata: alphabet extension and product.
引用
收藏
页码:156 / 170
页数:15
相关论文
共 50 条
  • [21] FROM NONDETERMINISTIC BUCHI AND STREETT AUTOMATA TO DETERMINISTIC PARITY AUTOMATA
    Piterman, Nir
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2007, 3 (03)
  • [22] On complementing nondeterministic Buchi automata
    Gurumurthy, S
    Kupferman, O
    Somenzi, F
    Vardi, MY
    [J]. CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, PROCEEDINGS, 2003, 2860 : 96 - 110
  • [23] Congruence Relations for Buchi Automata
    Li, Yong
    Tsay, Yih-Kuen
    Turrini, Andrea
    Vardi, Moshe Y.
    Zhang, Lijun
    [J]. FORMAL METHODS, FM 2021, 2021, 13047 : 465 - 482
  • [24] Determinization of Buchi-automata
    Roggenbach, M
    [J]. AUTOMATA, LOGICS, AND INFINITE GAMES: A GUIDE TO CURRENT RESEARCH, 2002, 2500 : 43 - 60
  • [25] From nondeterministic Buchi and Streett automata to deterministic parity automata
    Piterman, Nir
    [J]. 21ST ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2006, : 255 - 264
  • [26] Bounded Model Checking with SNF, Alternating Automata, and Buchi Automata
    Sheridan, Daniel
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 119 (02) : 83 - 101
  • [27] From LTL to unambiguous Buchi automata via disambiguation of alternating automata
    Jantsch, Simon
    Mueller, David
    Baier, Christel
    Klein, Joachim
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2021, 58 (1-2) : 42 - 82
  • [28] Abstract Interpretation from Buchi Automata
    Hofmann, Martin
    Chen, Wei
    [J]. PROCEEDINGS OF THE JOINT MEETING OF THE TWENTY-THIRD EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC (CSL) AND THE TWENTY-NINTH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2014,
  • [29] FIXED-POINTS OF BUCHI AUTOMATA
    DAM, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 652 : 39 - 50
  • [30] On the complementation of asynchronous cellular Buchi automata
    Muscholl, A
    [J]. THEORETICAL COMPUTER SCIENCE, 1996, 169 (02) : 123 - 145