PV5 ⊧ opaala lightweight variant of UPPAAL intended for rapid prototyping

Model checker for lattice automata

Application domain/field

• Lattice automata
• Model checking
• CEGAR (Counter-Example Guided Abstraction Refinement)
• UPPAAL

Type of tool

Model checker

Expected input

Format:

UPPAAL XML format extended with lattice features

Internals

"opaal is a distributed/parallel (discrete time) model checker for networks of timed automata..." (Source) Uses pyuppaal.