Testing Membership for Timed Automata

TL;DR

This paper introduces a testing method for timed automata that determines if a timed word belongs to the automaton's language or is far from it, using a new timed edit distance and finite sampling.

Contribution

It presents a novel tester for timed automata that leverages a new timed edit distance and finite sampling to decide membership or epsilon-far status.

Findings

Introduces a tester for timed automata membership.

Defines a new timed edit distance metric.

Provides a decision procedure using finite samples.

Abstract

Given a timed automata which admits thick components and a timed word $x$, we present a tester which decides if $x$ is in the language of the automaton or if $x$ is $\epsilon$-far from the language, using finitely many samples taken from the weighted time distribution $\mu$ associated with an input $x$. We introduce a distance between timed words, the {\em timed edit distance}, which generalizes the classical edit distance. A timed word $x$ is $\epsilon$-far from a timed language if its relative distance to the language is greater than $\epsilon$.