PV1 ⊧ TCheckercan compute reachable states and detect syntax errors of timed automata

Checks reachability for timed automata with diagonal constraints (and only resets as updates).

Application domain/field

• Reachability
• Timed automata
• Pushdown timed automata (PDTA)
• Model checking

Type of tool

Model checker

Expected input

Timed automaton, Optional flags available to e.g. choose a reachability algorithm, specify which state to compute reachability for, whether to use syntax check or to flatten the model, etc.

Format:

Own language

Expected output

Depends on the tool and flags that are used. tck-reach will compute the reachable states. tck-syntax will either (1) report syntax errors, or (2) computes a flattened model

Internals

TChecker consists of two tools:

• tck-reach for reachability analysis
• tck-syntax for analyses such as model transformation and syntax checks

Comments

License: MIT