S. Akshay ; Paul Gastin ; Shankara Narayanan Krishna - Analyzing Timed Systems Using Tree Automata

lmcs:3156 - Logical Methods in Computer Science, May 9, 2018, Volume 14, Issue 2 - https://doi.org/10.23638/LMCS-14(2:8)2018
Analyzing Timed Systems Using Tree AutomataArticle

Authors: S. Akshay ; Paul Gastin ; Shankara Narayanan Krishna

    Timed systems, such as timed automata, are usually analyzed using their operational semantics on timed words. The classical region abstraction for timed automata reduces them to (untimed) finite state automata with the same time-abstract properties, such as state reachability. We propose a new technique to analyze such timed systems using finite tree automata instead of finite word automata. The main idea is to consider timed behaviors as graphs with matching edges capturing timing constraints. When a family of graphs has bounded tree-width, they can be interpreted in trees and MSO-definable properties of such graphs can be checked using tree automata. The technique is quite general and applies to many timed systems. In this paper, as an example, we develop the technique on timed pushdown systems, which have recently received considerable attention. Further, we also demonstrate how we can use it on timed automata and timed multi-stack pushdown systems (with boundedness restrictions).


    Volume: Volume 14, Issue 2
    Published on: May 9, 2018
    Accepted on: April 12, 2018
    Submitted on: February 22, 2017
    Keywords: Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science,F.1.1

    1 Document citing this article

    Consultation statistics

    This page has been seen 1986 times.
    This article's PDF has been downloaded 784 times.