BayesianBreakfast

emptiness checker

• Can find details in emptiness_checker directory. Implements emptiness checker based on event clock automaton, and using the tchecker's GTA-model for the emptiness check.
• Details of running emptiness checker can be found at here

Special credits

• Using GTA-model as tool for checking emptiness for event clock automata.
• GTA-model uses tchecker as backbone.

Papers this is based on:

• Verifying Refinement of Probabilistic Contracts Using Timed Automata
• SIMULATIONS FOR EVENT-CLOCK AUTOMATA
• Event-clock automata: a determinizable class of timed automata