On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions

TL;DR

This paper introduces an on-the-fly symbolic algorithm for verifying timed ATL in real-time systems, utilizing abstractions and the ADG framework to significantly improve performance over existing methods.

Contribution

It presents a novel abstraction that eliminates the need for inclusion checks in timed ATL verification, leading to substantial efficiency gains.

Findings

Almost two orders of magnitude faster than naive methods

Outperforms Uppaal Tiga in verifying TATL

Improves Uppaal Tiga performance by nearly tenfold

Abstract

Verification of real-time systems with multiple components controlled by multiple parties is a challenging task due to its computational complexity. We present an on-the-fly algorithm for verifying timed alternating-time temporal logic (TATL), a branching-time logic with quantifiers over outcomes that results from coalitions of players in such systems. We combine existing work on games and timed CTL verification in the abstract dependency graph (ADG) framework, which allows for easy creation of on-the-fly algorithms that only explore the state space as needed. In addition, we generalize the conventional inclusion check to the ADG framework which enables dynamic reductions of the dependency graph. Using the insights from the generalization, we present a novel abstraction that eliminates the need for inclusion checking altogether in our domain. We implement our algorithms in Uppaal and our experiments show that while inclusion checking considerably enhances performance, our abstraction provides even more significant improvements, almost two orders of magnitude faster than the naive method. In addition, we outperform Uppaal Tiga, which can verify only a strict subset of TATL. After implementing our new abstraction in Uppaal Tiga, we also improve its performance by almost an order of magnitude.