xta

README.md — what this module is

Mirrored from subprojects/xta/xta/README.md — edit it there, not here.

Overview

This project contains the Uppaal timed automata (XTA) formalism. Its main purpose is to describe timed systems as graphs with clock variables. A domain specific language (DSL) is available to parse XTAs from the textual representation of Uppaal. The project contains:

• Classes to represent XTAs.
• A domain specific language (DSL) to parse XTAs from a textual representation.

Related projects

• xta-analysis: XTA specific analysis modules enabling the algorithms to operate on them.
• xta-cli: An executable tool (command line) for running analyses on XTAs.

Further reading

The full publication list is at theta.mit.bme.hu/publications.

Lazy abstraction for clocks

• Lazy Reachability Checking for Timed Automata using Interpolants (FORMATS 2017) — zone interpolation to strengthen the abstraction.
• Lazy Reachability Checking for Timed Automata with Discrete Variables (SPIN 2018) — combining data abstraction with lazy abstraction for clocks.
• Configurable verification of timed automata with discrete variables (Acta Informatica 2020) — the configurable framework, integrating LU-bound-based lazy abstraction; the journal version of the line above.
• Timed Automata Verification using Interpolants (Minisy 2017) — interpolation over difference bound matrices.
• Generalizing lazy abstraction refinement algorithms with partial orders (BSc, 2021) — a configurable lazy abstraction framework built on partial orders and Galois connections.

Other refinement strategies

• Backward reachability analysis for timed automata with data variables (AVoCS 2018) — handling data variables with the weakest precondition operation.
• Activity-Based Abstraction Refinement for Timed Systems (Minisy 2017) — refinement tailored to clock variables.
• Verification of Timed Automata by CEGAR-Based Algorithms (MSc, 2016).

Models, benchmarks and applications

• Formal Modeling of Real-Time Systems with Data Processing (Minisy 2016) — a formalism covering both timing and data.
• Towards Reliable Benchmarks of Timed Automata (Minisy 2018) — the benchmark suite used to compare these algorithms.
• Abstraction-based timed model checking for software-intensive system models (MSc, 2023) — timed verification without discretization.