Reading Guide

This section is the concept-oriented companion to Installation. It is not mainly about installation steps or command sequences. Its job is to explain what the core UPPAAL concepts mean, why they are needed, and how they connect to the Python-facing direction of pyudbm.

How To Use This Section

Use this section when you are asking questions such as:

  • What problem is UPPAAL trying to solve?

  • Why is time harder than ordinary finite-state verification?

  • Why do symbolic states, zones, DBMs, and federations appear at all?

  • Which concepts do I need before the high-level Python API starts to feel natural?

If you only want to install the package or run a quick smoke check, start with Installation instead.

Reading Routes

This entry page is meant to be a reading router rather than a flat directory. Different readers should start in different places.

If you are new to formal verification or model checking:

Start with What Is UPPAAL?.

If you already know what model checking is, but timed automata still feel unfamiliar:

Start with What Is UPPAAL?, then continue to Timed Automata.

If you already know the model shape, but you are still unsure how requirements are phrased:

Continue from Timed Automata to Queries and Properties.

If you already know timed automata, but symbolic states and zones still feel abstract:

Read What Is UPPAAL? for the big-picture workflow first, then continue to Symbolic States and Zones and DBM Basics.

If you already know zones and DBMs, but do not yet see why non-convex symbolic sets matter:

Skim What Is UPPAAL?, then continue to Federations: Exact Unions Of DBM Zones and CDD Basics: How Shared Decision Graphs Compress Non-Convex Symbolic Sets.

If your main concern is the future Python-facing architecture of this repository:

Read What Is UPPAAL? first, because it explains the user-facing verification workflow that the restored Context / Clock / Federation model is trying to serve.

Current Coverage

Planned Sequence

The current concept roadmap is:

  • what-is-uppaal/

  • timed-automata/

  • queries-and-properties/

  • symbolic-states/

  • dbm-basics/

  • federations/

  • cdd/

  • search / extrapolation / storage topics

  • reduction-oriented topics

  • priced timed automata and API reconstruction topics

How This Relates To Other Doc Areas

The three documentation areas serve different jobs:

  • Installation answers “How do I install or build it?”

  • foundations/ answers “What do these concepts mean?”

  • papers/ in the repository answers “Which papers and reading guides are these explanations based on?”

For this repository in particular, that separation matters. pyudbm is not trying to be a complete UPPAAL clone today, but it is trying to rebuild a thin, high-level Python surface on top of the UDBM layer in a way that still makes sense inside the larger UPPAAL story.