
LARVA
 Referenced in 6 articles
[sw21408]
 number of notations, including timedautomata enriched with stopwatches, Lustre, and a subset of duration ... transactions. LARVA also performs analysis of realtime properties, to calculate, if possible, an upper...

GEZEL
 Referenced in 6 articles
[sw04151]
 relate this domain to the timedautomata model and we have experimented with verification...

COSMOS
 Referenced in 5 articles
[sw13329]
 eralization of Deterministic Timed Automata (DTA), to describe relevant execution paths of a Discrete Event...

REDLIB
 Referenced in 5 articles
[sw21175]
 full TCTL modelchecking of densetime automata with multiple fairness assumptions. REDLIB uses ... efficient representation and manipulation of densetime statespaces. Users can use the procedures in REDLIB...

Casaal
 Referenced in 5 articles
[sw10130]
 approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric ... WMTL ≤ , allowing for efficient SMC by runtime evaluation of a given formula. By necessity...

LiQuor
 Referenced in 18 articles
[sw04136]
 omegaregular linear time properties by means of automatabased model checking algorithms...

PEPS
 Referenced in 34 articles
[sw03186]
 Automata Networks(SAN) models. In its sequential version, the cost of the execution time becomesimpracticable...

mctau
 Referenced in 2 articles
[sw07213]
 formal semantics in terms of stochastic timed automata, an overarching formalism of which several well ... paper, we focus on networks of timed automata as supported by Uppaal. We report ... subset of Modest models to Uppaal timed automata and enable connections to further tools...

McAiT
 Referenced in 3 articles
[sw09947]
 McAiT is that it leverages timed automata to model both the timing behaviors...

Timed Automata
 Referenced in 1 article
[sw28568]
 Timed automata are a widely used formalism for modeling realtime systems, which is employed ... subclass of diagonalfree timed automata, which is sufficient to model many interesting problems ... concepts and semantics of diagonalfree timed automata. Based on this, we prove two types...

DCVALID
 Referenced in 14 articles
[sw20416]
 based on an automata theoretic decision procedure for Quantified Discretetime Duration Calculus (QDDC ... efficient multiterminal BDD based representation of automata and has implemented algorithms for operations...

Calife
 Referenced in 1 article
[sw28607]
 several automata models (transition systems, timed automata, counter automata,...) and allows to define new models ... Kronos, CMC, Coq,...) and a unique timedautomata system modelled under the Calife System Editor...

HighSpec
 Referenced in 1 article
[sw09750]
 combination of ObjectZ (OZ) and Timed Automata (TA). Building on the strength of Object ... specifying data structures and Timed Automata’s in modelling dynamic and realtime behaviors, OZTA...

CATS
 Referenced in 1 article
[sw17954]
 realtime systems modeled using timed automata and the realtime calculus. It is based...

TarTar
 Referenced in 1 article
[sw37080]
 TarTar: a timed automata repair tool. We present TarTar, an automatic repair analysis tool that...

ZenoTool
 Referenced in 1 article
[sw10129]
 tool that analyzes model specifications of timed automata systems created with UPPAAL for the occurrence ... Runs. Zeno Runs are paths in the timed transition system where infinite actions are executed...

Time4sys2imi
 Referenced in 1 article
[sw31184]
 tool translating Time4sys models into parametric timed automata in the input language of IMITATOR. This ... only to check the schedulability of realtime systems, but also to infer some timing...

ltl2dstar
 Referenced in 4 articles
[sw21007]
 converts formulas in Linear Time Logic to deterministic ωautomata, specifically Rabin (DRA) and Streett...

DYANA
 Referenced in 1 article
[sw36150]
 also transformed into a Network of Timed Automata (NTA). After translation into...

Moby/DC
 Referenced in 5 articles
[sw01395]
 realtime specifications. We define an operational subset of Duration Calculus, called phase automata, which ... realtime system descriptions that contain timing parameters. We introduce the tool MOBY/DC which implements ... modelchecking algorithm for phase automata. The algorithm applies compositional modelchecking techniques and handles...