Dynamic Data Structures for Timed Automata Acceptance

被引:0
|
作者
Alejandro Grez
Filip Mazowiecki
Michał Pilipczuk
Gabriele Puppis
Cristian Riveros
机构
[1] Pontificia Universidad Católica de Chile,
[2] Millennium Institute for Foundational Research on Data,undefined
[3] University of Warsaw,undefined
[4] University of Udine,undefined
来源
Algorithmica | 2022年 / 84卷
关键词
Timed automata; Data stream; Dynamic data structure; Theory of computation; Models of computation;
D O I
暂无
中图分类号
学科分类号
摘要
We study a variant of the classical membership problem in automata theory, which consists of deciding whether a given input word is accepted by a given automaton. We do so through the lenses of parameterized dynamic data structures: we assume that the automaton is fixed and its size is the parameter, while the input word is revealed as in a stream, one symbol at a time following the natural order on positions. The goal is to design a dynamic data structure that can be efficiently updated upon revealing the next symbol, while maintaining the answer to the query on whether the word consisting of symbols revealed so far is accepted by the automaton. We provide complexity bounds for this dynamic acceptance problem for timed automata that process symbols interleaved with time spans. The main contribution is a dynamic data structure that maintains acceptance of a fixed one-clock timed automaton A\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathcal {A}}$$\end{document} with amortized update time 2O(|A|)\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$2^{{\mathcal {O}}(|{\mathcal {A}}|)}$$\end{document} per input symbol.
引用
收藏
页码:3223 / 3245
页数:22
相关论文
共 50 条
  • [1] Dynamic data structures for timed automata acceptance
    Grez, Alejandro
    Mazowiecki, Filip
    Pilipczuk, Michal
    Puppis, Gabriele
    Riveros, Cristian
    [J]. Leibniz International Proceedings in Informatics, LIPIcs, 2021, 214
  • [2] Dynamic Data Structures for Timed Automata Acceptance
    Grez, Alejandro
    Mazowiecki, Filip
    Pilipczuk, Michal
    Puppis, Gabriele
    Riveros, Cristian
    [J]. ALGORITHMICA, 2022, 84 (11) : 3223 - 3245
  • [3] Data-structures for the verification of timed automata
    Asarin, E
    Bozga, M
    Kerbrat, A
    Maler, O
    Pnueli, A
    Rasse, A
    [J]. HYBRID AND REAL-TIME SYSTEMS, 1997, 1201 : 346 - 360
  • [4] Reachability results for timed automata with unbounded data structures
    Ruggero Lanotte
    Andrea Maggiolo-Schettini
    Angelo Troina
    [J]. Acta Informatica, 2010, 47 : 279 - 311
  • [5] Reachability results for timed automata with unbounded data structures
    Lanotte, Ruggero
    Maggiolo-Schettini, Andrea
    Troina, Angelo
    [J]. ACTA INFORMATICA, 2010, 47 (5-6) : 279 - 311
  • [6] VERIFICATION FOR TIMED AUTOMATA EXTENDED WITH UNBOUNDED DISCRETE DATA STRUCTURES
    Quaas, Karin
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (03)
  • [7] Timed automata with data structures for distributed systems design and analysis
    Lanotte, R
    Maggiolo-Schettini, A
    Troina, A
    [J]. SEFM 2005: THIRD IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2005, : 44 - 53
  • [9] Translation of Timed Promela to Timed Automata with Discrete Data
    Nabialek, Wojciech
    Janowska, Agata
    Janowski, Pawel
    [J]. FUNDAMENTA INFORMATICAE, 2008, 85 (1-4) : 409 - 424
  • [10] Efficient verification of timed automata with BDD-like data-structures
    Wang, F
    [J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, 2003, 2575 : 189 - 205