Event-Clock Nested Automata

TL;DR

This paper introduces Event-Clock Nested Automata (ECNA), a formalism combining real-time properties with recursive program patterns, maintaining key decidability and closure properties, and extending previous models.

Contribution

The paper defines ECNA, demonstrating their closure properties, decidability, and expressiveness, advancing the formal analysis of real-time recursive systems.

Findings

ECNA are closed under Boolean operations.

Emptiness, universality, and inclusion are EXPTIME-complete for ECNA.

ECNA extend previous models combining ECA and VPA.

Abstract

In this paper we introduce and study Event-Clock Nested Automata (ECNA), a formalism that combines Event Clock Automata (ECA) and Visibly Pushdown Automata (VPA). ECNA allow to express real-time properties over non-regular patterns of recursive programs. We prove that ECNA retain the same closure and decidability properties of ECA and VPA being closed under Boolean operations and having a decidable language-inclusion problem. In particular, we prove that emptiness, universality, and language-inclusion for ECNA are EXPTIME-complete problems. As for the expressiveness, we have that ECNA properly extend any previous attempt in the literature of combining ECA and VPA.