Our goal is to develop a full working solver for ATA (with 1 clock) in Python, with MTL to ATA support. The decidability for the emptiness problem was proposed by Lasota and Walukiewicz. The MTL to ATA was proposed by Ouaknine and Worrell.
- Alternating Timed Automata emptiness solver
- MTL to ATA translation
- Common ATA operations (Union, Complementation, Intersection, Model checking)
Be the first to post a review of Alternating Timed Automata Solver!