UPPAAL

UPPAAL is a handy tool for modeling, validating, and checking real-time systems. It works by using networks of timed automata and even adds some cool data types like bounded integers and arrays.

What is UPPAAL CORA?

Now, there’s a special version called UPPAAL CORA. It focuses on Cost Optimal Reachability Analysis and was developed by the UPPAAL team as part of the VHS and AMETIST projects. Unlike the regular UPPAAL that checks models of timed automata, UPPAAL CORA uses something called LPTA. This lets you add cost details to your models.

Understanding Costs

This cost could represent delays in specific situations or the costs linked to certain actions. With UPPAAL CORA, you can find the best paths that meet your goal conditions.

Real-World Uses

People have used UPPAAL CORA in various case studies! If you have some interesting applications in mind, feel free to reach out. We’d love to hear what you're doing!

Two Versions Available

The current version of UPPAAL CORA has two different setups:

• A simple case for time optimal reachability analysis.


• A complete version using the full language of LPTA.

Free for Non-Profit Use!

Just like UPPAAL, you can use UPPAAL CORA for free if it’s for non-profit activities like research or teaching!

Main Features to Note:

• The modeling language in UPPAAL CORA adapts easily if your problem changes. So no worries about losing all that hard work!


• This tech may be new and different from what we usually see in operational research, but it's proven competitive in various studies.


• The language of UPPAAL CORA covers everything from regular UPPAAL models. That means you can reuse your existing models without starting over!


• This tool includes recent updates and performance boosts from the latest version of UPPAAL but keep in mind it's still experimental.

A Few Limitations

• No extrapolation yet—so make sure your system is acyclic or all clocks are bounded by invariants if you want termination guaranteed.


• You can only do simple reachability checks right now—no liveness or deadlock checks yet.


• The guiding features are limited; while it supports sorting based on cost plus remaining aspects (best first search), there are some constraints on how heuristic variables work with costs.

This Release Fixes Issues:

• This latest release fixes crash bugs and gets rid of a memory leak too!