Perfect languages, characterized by closure under Boolean operations and decidable emptiness problem, form the basis for decid-able automata-theoretic model-checking for the corresponding class of models. Regular languages and visibly pushdown languages are paradigmatic examples of perfect languages. In a previous work authors have established a timed context-sensitive perfect language characterized by multistack pushdown automata (MPA) with an explicit bound on number of rounds where in each round at most one stack is used. This paper complements the results of on bounded-round timed MPA by characterizing an alternative restriction on timed context-sensitive perfect languages called the scope-bounded multi-stack timed push-down automata where every stack symbol must be popped within a bounded number of stack contexts. The proposed model uses visibly-pushdown alphabet and event clocks to recover a bounded-scope MPA with decidable emptiness, closure under Boolean operations, and an equivalent logical characterization.
展开▼
