一句话：提出用有限树自动机分析时间系统，将时间行为编码为有界树宽的图，从而用MSO与树自动机判定性质。
时间系统（如时间自动机）通常基于时间字上的操作语义分析，经典区域抽象将其归约为有限字自动机，以保持状态可达性等时间抽象性质。本文提出改用有限树自动机：将时间行为视为带匹配边的图，其中匹配边刻画时序约束；当这类图族具有有界树宽时，可解释到树上，并用树自动机检查其MSO可定义性质。该技术具有通用性，作者以时间下推系统为例展开，并展示其可应用于时间自动机以及带界限制的时间多栈下推系统。
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).
@article{paperbot407,
title = {Analyzing Timed Systems Using Tree Automata},
author = {S. Akshay and Paul Gastin and Shankara Narayanan Krishna},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 2},
year = {2018},
doi = {10.23638/lmcs-14(2:8)2018}
}