alternating timed automata solver

We have hosted the application alternating timed automata solver in order to run this application in our online workstations with Wine or directly.

Quick description about alternating timed automata solver:

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.

Features:

• Alternating Timed Automata emptiness solver
• MTL to ATA translation
• Common ATA operations (Union, Complementation, Intersection, Model checking)

Audience: Information Technology.
User interface: Qt.
Programming Language: Python.
Database Environment: XML-based.
.