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)

Project Activity

See All Activity >

License

GNU General Public License version 3.0 (GPLv3)

Follow Alternating Timed Automata Solver

Alternating Timed Automata Solver Web Site

Other Useful Business Software
PRTG Catches Network Issues Before They Cause Downtime Icon
PRTG Catches Network Issues Before They Cause Downtime

Threshold-based alerts flag problems early, so your team can act before users notice, not after.

Reactive troubleshooting usually means hearing about a problem from frustrated users, not your monitoring tool. PRTG sets threshold-based alerts across devices, servers and applications, notifying your team by email, SMS or push the moment a metric crosses a set limit. That means catching a failing disk or overloaded server before it becomes an outage and getting time back from firefighting. Start a free trial and set your first alerts today.
Download 30-Day Trial
Rate This Project
Login To Rate This Project

User Reviews

Be the first to post a review of Alternating Timed Automata Solver!

Additional Project Details

Languages

English, Italian

Intended Audience

Information Technology

User Interface

Qt

Programming Language

Python

Database Environment

XML-based

Related Categories

Python UML Tool, Python Scientific Engineering, Python Libraries

Registered

2010-02-04