Modelling nondeterminism: transition systems and Petri Nets

1. From specifications to behaviour models

This chapter opens Part C of the course and turns the specification machinery of chapter 6 into a general framework for behaviour. Deck 06, "Modelling evolving systems and unbounded size: a programming language approach", starts from a sharp claim about what software models are:

"Software models are specification of a software systems, useful for design and verification" · "software models capturing system behaviour are systems per se, to be properly engineered" · "programming languages (like Scala) are very good at programming software models".

Three sentences, three commitments. A model is useful because it supports both design (building the right system) and verification (checking the system is right). A behavioural model is not a passive drawing: it is a computational system itself, which means it can be run, animated, simulated and analysed — and therefore it deserves the same engineering care as any other code. And the tool of choice for engineering it is a programming language, because the model is a specification, and a specification is code.

The previous case of specification language in the course was the axiom-based ADT, which chapter 6 turned into Scala ADTs with traits, opaque types, and ScalaCheck/Test. The canonical example is the List[A] ADT: a type, constructors (cons, nil), an operation (concat), and two axioms:

type:        List[A]
constructors: cons: A x List[A] => List[A]   nil: List[A]
operations:  concat: List[A] x List[A] => List[A]
axioms:
  [A1] concat(nil, l) = l
  [A2] concat(cons(h, t), l) = cons(h, concat(t, l))

The move of the lecture is to read this ADT as a computational system in its own right, and to generalise from it:

• Syntax — the states are all the expressions, i.e. all typed combinations of cons, nil and concat;
• Computation semantics — each left-to-right single axiom application is a computational step;
• Complete computation — a computation that reaches a final expression no longer reducible;
• Result of computation — the final expression, if it is made by constructors only;
• Error of computation — the final expression, if it is made not only by constructors;
• Non-termination — there exists an infinite sequence of steps;
• Non-determinism — there may be two (or more) possible steps at a certain expression.

The example derivation shows all of these notions at once. Start from concat(nil, concat(cons(10, nil), cons(20, nil))), apply A1 with l = concat(cons(10, nil), cons(20, nil)), then A2 with h = 10, t = nil, l = cons(20, nil), then A1 again, and the computation stops at cons(10, cons(20, nil)) — a normal form, and a legal result because it is made of constructors only:

concat(nil, concat(cons(10, nil), cons(20, nil)))
  --> A1: l = concat(cons(10, nil), cons(20, nil))
concat(cons(10, nil), cons(20, nil))
  --> A2: h = 10, t = nil, l = cons(20, nil)
cons(10, concat(nil, cons(20, nil)))
  --> A1: l = cons(20, nil)
cons(10, cons(20, nil))
  --| normal form reached

The deck then poses the questions that drive the whole part: are there other specific models for interesting systems? how do we "scale" to specify behaviour of large IoT systems? which sources of complexity/uncertainty need to be considered? The rest of this chapter answers the first two with the framework of transition systems and with Petri Nets; the third question is the bridge to chapter 10.

2. The framework of reduction systems

The general framework is introduced as a reduction/rewrite/transition system (RS), and the lecture is careful to give the formal definition before any pragmatics:

An RS is a couple ⟨S, →⟩, where: S is a denumerable set of states; → ⊆ S × S is the rewrite relation. Use notation S → S′ to mean ⟨S, S′⟩ ∈ →: from state S we can move to S′. Namely, this is a (possibly infinite) graph, called the rewrite graph.

That is all there is. S encodes the system structure/state at a given time, → encodes the dynamics; the couple is a directed graph, and the graph may be infinite. From this couple, the deck derives the vocabulary used throughout the course:

• Reachability — s is reachable from s0 (written s0 →* s) if there is a path s0 → s1 → s2 → ... → sn = s (n ≥ 0); the reachability set of s, denoted RS(s), is the set of states reachable from s;
• Non-deterministic system — if for some s there are distinct s1 and s2 such that s → s1 and s → s2;
• Confluent system ("don't-care non-determinism") — if for any s, s1, s2 with s →* s1 and s →* s2 there exists s3 with s1 →* s3 and s2 →* s3;
• Normal form (or deadlock) — s is a normal form if s ↛ (no outgoing steps);
• Church–Rosser property — given an s0, confluent systems have at most one reachable normal form.

The abstraction is deliberately minimal, and that is its power: it captures ADTs and every other behaviour model of the course, it is the general framework in which model-checking logics such as LTL/CTL are defined (for "bounded" model-checking, i.e. when S is essentially finite), and it will be extended with probabilities and rates in chapter 10.

An example with extensional specification: a communication end-point

The deck's first example is a communication end-point formalised by listing the states and the relation:

S = {s0, s1, s2, s3}
→ = {s0 → s1, s1 → s1, s1 → s3, s3 → s3, s1 → s2, s2 → s1}
// sometimes the initial state is explicitly denoted

The example is the first appearance of a pattern that will recur in every chapter of this part: the same five states will later be re-labelled as IDLE, SEND, DONE, FAIL and given rates in chapter 10 (the stochastic channel), and the same graph will be the running example for CTL and PCTL model-checking in chapter 11.

3. Extensional versus intensional specification

Listing all pairs of the relation works when the system is small, but the deck is explicit about why it does not scale:

• the number of states may be too big to write down the RS extensionally;
• the number of states may simply be infinite;
• one wants to capture recurrent patterns and apply the DRY principle — and "even a specification is code, it must be clean!"

The two styles of specification are given formal names:

Extensional specification: listing all S, S′ such that S → S′.

Intensional specification: S by a grammar (syntax), → by deduction rules (operational semantics).

The ADT of section 1 is intensional: the syntax (cons, nil, concat) is a grammar over an infinite set of expressions, and the axioms A1/A2 are deduction rules that define one step. The mutual-exclusion system of section 5 is intensional in a different way: the state space is finite but combinatorial (all configurations of n processes), too large to enumerate by hand, so the transition relation is given by a few rule schemata.

4. Programming transition systems in Scala

The lecture now makes the meta-modelling claim concrete. There are three modelling levels, and Scala sits at the top of all of them:

• meta-meta-model — the nature of computation: reduction-system semantics;
• meta-model — the class of computation: ADTs (extensional), Petri Nets, and so on;
• model — the specific computation: the List ADT, the channel, mutual exclusion.

Why is a meta-modelling framework useful? The deck lists five benefits: computing abstractions are naturally defined mathematically; translating the math into a computational meta-framework is interesting and useful — "computer scientists and engineers may understand it better", "it supports some check of correctness of the mathematical descriptions", "it allows you to put those concepts in practice", "it allows you to 'simulate/run' those computing abstractions", "it allows you to enact forms of model-driven engineering". And why Scala? "Those meta-frameworks need to have rich type systems, DSL support, and be expressive, flexible" — "Scala (3+) is proved rather effective, as it brings us close to math."

The System type and its factory

The meta-meta-model is one trait: a rewrite system is exactly a function from a state to its possible next states — S => Set[S]. The deck notes that a System is substitution-equivalent to S => Set[S].

// The definition of a Rewrite System, as a function: S => Set[S]
trait System[S]:
  def next(a: S): Set[S]

// Our factory of Systems
object System:

  // The most general case, an intensional one
  def ofPartialFunction[S](f: PartialFunction[S, Set[S]]): System[S] = s =>
    f.applyOrElse(s, _ => Set[S]())

  // Extensional specification
  def ofRelation[S](rel: Set[(S, S)]): System[S] = ofPartialFunction: s =>
    rel collect:
      case (`s`, s2) => s2

  // Extensional with varargs
  def ofTransitions[S](rel: (S, S)*): System[S] =
    ofRelation(rel.toSet)

The factory offers three ways to build a system: ofPartialFunction for the most general intensional case (with applyOrElse defaulting to the empty set), ofRelation for an extensional specification as a set of pairs, and ofTransitions for the same thing with varargs sugar.

SystemAnalysis: querying a system

Analysis is an extension that "empowers" System. A Path is a List[S]; normalForm asks whether a state has no successors; complete asks whether a path ends in a normal form; paths generates all paths of exactly depth steps; completePathsUpToDepth filters complete paths up to a depth (the deck notes it "could be optimised"):

// Basical analysis helpers
object SystemAnalysis:

  type Path[S] = List[S]

  extension [S](system: System[S])

    def normalForm(s: S): Boolean = system.next(s).isEmpty

    def complete(p: Path[S]): Boolean = normalForm(p.last)

    // paths of exactly length 'depth'
    def paths(s: S, depth: Int): Seq[Path[S]] = depth match
      case 0 => LazyList()
      case 1 => LazyList(List(s))
      case _ =>
        for
          path <- paths(s, depth - 1)
          next <- system.next(path.last)
        yield path :+ next

    // complete paths with length '<= depth' (could be optimised)
    def completePathsUpToDepth(s: S, depth: Int): Seq[Path[S]] =
      (1 to depth).to(LazyList) flatMap (paths(s, _)) filter (complete(_))

Technical notes from the deck: Path could have been made opaque but that is not very useful here; SystemAnalysis "empowers" System via the extension; the examples use export to make a self-contained import unit; and the test syntax is the "fancy syntax in AnyFunSuite".

The channel as an example

The communication end-point of section 2 becomes a runnable object. Note the exports: the object exposes the State enum cases and all of SystemAnalysis, so the main reads like a query session.

object SystemChannel:

  // Specification of a data-type for channel states
  enum State:
    case IDLE, SEND, DONE, FAIL

  // enabling analysis through this object
  export u06.modelling.SystemAnalysis.*
  export State.*

  // System specification
  def channel: System[State] = System.ofTransitions(
    IDLE -> SEND,
    SEND -> SEND, SEND -> DONE, SEND -> FAIL,
    FAIL -> IDLE // , DONE -> DONE
  )

@main def mainSystemChannel() =
  import SystemChannel.*
  // Analysis, by querying
  println(channel.normalForm(IDLE))
  println(channel.normalForm(DONE))
  println(channel.next(IDLE))
  println(channel.next(SEND))
  println("P1 " + channel.paths(IDLE, 1).toList)
  println("P2 " + channel.paths(IDLE, 2).toList)
  println("P3 " + channel.paths(IDLE, 3).toList)
  println("P4 " + channel.paths(IDLE, 4).toList)
  println("CMP:\n" + channel.completePathsUpToDepth(IDLE, 10).mkString("\n"))

Note the deliberate comment // , DONE -> DONE: as specified, DONE is a normal form — there is no outgoing transition — while every other state moves on. That is what the analysis prints: normalForm(IDLE) is false, normalForm(DONE) is true, next(SEND) is Set(SEND, DONE, FAIL), and the complete paths up to depth 4 are exactly List(IDLE, SEND, DONE) and List(IDLE, SEND, SEND, DONE).

The corresponding ScalaTest suite pins these answers as the contract of the model — this is the pervasive-validation discipline of chapter 1 applied to a specification:

import org.scalatest.funsuite.AnyFunSuite
import org.scalatest.matchers.should.Matchers.*

class SystemChannelSpec extends AnyFunSuite:
  import u06.examples.SystemChannel.*

  test("System Channel should properly identify normal forms"):
    channel.normalForm(IDLE) shouldBe false
    channel.normalForm(DONE) shouldBe true

  test("System Channel should properly draw next states"):
    channel.next(IDLE) shouldBe Set(SEND)
    channel.next(SEND) shouldBe Set(SEND, DONE, FAIL)

  test("System Channel should properly generate paths"):
    channel.paths(IDLE, 3) should contain:
      List(IDLE, SEND, SEND)
    channel.completePathsUpToDepth(IDLE, 4) should contain theSameElementsAs:
      List(List(IDLE, SEND, DONE), List(IDLE, SEND, SEND, DONE))

5. Intensional specification at work: mutual exclusion

The deck poses the scaling question with a classic problem: "A mutual exclusion problem for n processes — what about n ≫ 2?" For two processes one could list the states and transitions by hand; for thousands of devices, extensional specification is hopeless. The answer is an intensional specification: states are configurations, and transitions are rule schemata.

Each process is in one of three states — N (non-critical / neutral), T (trying, i.e. asking to enter), C (critical) — and a global state is a List[State], one entry per process. The helper move replaces the first occurrence of a given state with another, returning the set of all such one-process updates; the system specification is then three lines that capture the rules:

object SystemMutualExclusion:

  enum State:
    case N, T, C

  export State.*
  export u06.modelling.SystemAnalysis.*

  type States = List[State]

  // helper
  private def move(l: States)(from: State, to: State): Set[States] =
    (0 until l.size).toSet.collect:
      case i if l(i) == from => l.updated(i, to)

  // System specification, try to capture the abstraction a bit
  def mutualExclusion: System[States] = l =>
    move(l)(N, T) ++ move(l)(C, N) ++ (if (l.contains(C)) Set() else move(l)(T, C))

@main def mainSystemMutualExclusion() =
  import SystemMutualExclusion.*
  println(mutualExclusion.next(List(N, N, N)))
  println(mutualExclusion.next(List(N, T, T)))
  println(mutualExclusion.next(List(N, T, C)))

  println(mutualExclusion.paths(List(N, N, N), 5).toList)
  println(mutualExclusion.paths(List(N, N, N), 5).contains:
    List(List(N, N, N), List(T, N, N), List(T, T, N), List(C, T, N), List(N, T, N)))

The three rules read as natural language: any N may move to T (a process starts trying); any C moves back to N (a process leaves the critical section); and — only if nobody is in C — any T may move to C. The if (l.contains(C)) Set() else ... guard is the mutual-exclusion condition itself, and it is the whole point of the model: the rule set defines the safety property rather than leaving it to chance.

The queries show the machinery: next(List(N, N, N)) contains the three single-process moves to T — any neutral process may start trying; next(List(N, T, T)) is Set(List(T, T, T), List(N, C, T), List(N, T, C)) — the remaining N may try, and either of the two Ts may enter the critical section, since nobody holds C; next(List(N, T, C)) allows only C → N, because the T → C move is blocked by the guard while C is occupied. The safety property is not a decoration: it is the guard, and the system's behaviour is defined by it.

6. Petri Nets: markings, transitions, unbounded size

Petri Nets are introduced as "a way of 'compiling' certain RS": instead of a set of states with a relation, the state space is generated from a few ingredients. The deck's formulation:

• S is the set of markings over the available places;
• a marking M is a multiset of places (names) — written like n|n|t|c;
• → can be defined by rules of a deduction system, one per transition.

The mutual-exclusion net is given by four deduction rules, the last with a condition — this is the inhibitor arc:

⊢ M → M|n          (spawn: a new process appears in N)
⊢ M|n → M|t        (N → T: a process starts trying)
⊢ M|c → M|n        (C → N: a process leaves the critical section)
⊢ M|c → M          (C consumed — process ends)
⊢ M|t → M|c  if c ∉ M   (T → C, allowed only when no C token is present)

For instance, one can derive ⊢ n|n|t|c → n|t|t|c: from a marking with two ns, a t and a c, the rule M|n → M|t fires on one of the n tokens. Crucially, because markings are multisets and the number of tokens is not bounded a priori, this is a Petri-Net for an unbounded mutual exclusion system: any number of processes can be represented, which is exactly what the extensional SystemMutualExclusion cannot do for n ≫ 2.

Modelling multisets: MSet

Since markings are multisets, the lab toolkit ships a small MSet abstraction. Its interface is functional: union, diff, disjoined, size, matches, extract, plus conversions (asList, asMap, iterator) and the fact that it is a function A => Int (the multiplicity of each element):

// A multiset datatype
trait MSet[A] extends (A => Int):
  def union(m: MSet[A]): MSet[A]
  def diff(m: MSet[A]): MSet[A]
  def disjoined(m: MSet[A]): Boolean
  def size: Int
  def matches(m: MSet[A]): Boolean
  def extract(m: MSet[A]): Option[MSet[A]]
  def asList: List[A]
  def asMap: Map[A, Int]
  def iterator: Iterator[A]

// Functional-style helpers / implementation
object MSet:
  // Factories
  def apply[A](l: A*): MSet[A] = new MSetImpl(l.toList)
  def ofList[A](l: List[A]): MSet[A] = new MSetImpl(l)
  def ofMap[A](m: Map[A, Int]): MSet[A] = MSetImpl(m)

  // Hidden reference implementation
  private case class MSetImpl[A](asMap: Map[A, Int]) extends MSet[A]:
    def this(list: List[A]) = this(list.groupBy(a => a).map((a, n) => (a, n.size)))
    override val asList = asMap.toList.flatMap((a, n) => List.fill(n)(a))
    override def apply(v1: A) = asMap.getOrElse(v1, 0)
    override def union(m: MSet[A]) = new MSetImpl[A](asList ++ m.asList)
    override def diff(m: MSet[A]) = new MSetImpl[A](asList diff m.asList)
    override def disjoined(m: MSet[A]) = (asList intersect m.asList).isEmpty
    override def size = asList.size
    override def matches(m: MSet[A]) = extract(m).isDefined
    override def extract(m: MSet[A]) = Some(this diff m).filter(_.size == size - m.size)

Read extract carefully: matches asks whether m is contained in this, and extract removes m from this — returning None exactly when the subtraction would have consumed tokens that were not there. That single operation is the "enabling test" of every transition in the framework.

7. Compiling Petri Nets into Systems

With System and MSet in hand, a Petri Net becomes a factory of Systems. The ingredients, per the deck:

• a state is a multiset of places (a marking);
• a transition is a tuple of multisets: pre-conditions (incoming arcs) and effects (outgoing arcs);
• inhibitory arcs require an additional element;
• we "just need to define a factory to create a System from a set of transitions".

import u06.utils.MSet

object PetriNet:
  // pre-conditions, effects, inhibition
  case class Trn[P](cond: MSet[P], eff: MSet[P], inh: MSet[P])
  type PetriNet[P] = Set[Trn[P]]
  type Marking[P] = MSet[P]

  // factory of a Petri Net
  def apply[P](transitions: Trn[P]*): PetriNet[P] = transitions.toSet

  // factory of a System, as a toSystem method
  extension [P](pn: PetriNet[P])
    def toSystem: System[Marking[P]] = m =>
      for
        Trn(cond, eff, inh) <- pn     // get any transition
        if m disjoined inh            // check inhibition
        out <- m extract cond         // remove precondition
      yield out union eff             // add effect

  // fancy syntax to create transition rules
  extension [P](self: Marking[P])
    def ~~>(y: Marking[P]) = Trn(self, y, MSet())
  extension [P](self: Trn[P])
    def ^^^(z: Marking[P]) = self.copy(inh = z)

The toSystem method is the "compiler": given a marking m, for each transition Trn(cond, eff, inh), it checks that m is disjoint from the inhibitor places, extracts the precondition (failing if it is not present — the for comprehension silently skips), and produces the new marking out union eff. The two extensions provide the DSL: MSet(N) ~~> MSet(T) reads "a token in N becomes a token in T", and ^^^ MSet(C) attaches the inhibitor. The mutual-exclusion net is then a single expression:

object PNMutualExclusion:

  enum Place:
    case N, T, C

  export Place.*
  export u06.modelling.PetriNet.*
  export u06.modelling.SystemAnalysis.*
  export u06.utils.MSet

  // DSL-like specification of a Petri Net
  def pnME = PetriNet[Place](
      MSet(N) ~~> MSet(T),
      MSet(T) ~~> MSet(C) ^^^ MSet(C),
      MSet(C) ~~> MSet()
  ).toSystem

@main def mainPNMutualExclusion =
  import PNMutualExclusion.*
  // example usage
  println(pnME.paths(MSet(N, N), 7).toList.mkString("\n"))

Compare with the hand-written SystemMutualExclusion of section 5: the Petri-Net version is three lines, the mutual-exclusion constraint is the inhibitor arc (^^^ MSet(C)) instead of an explicit if contains(C) guard, and the state space is now unbounded — paths(MSet(N, N), 7) already explores a tree of any number of tokens. The deck is explicit about what this buys: "it is essentially an executor/animator of petri nets", "the ability to draw next states could be the basis for a distributed implementation of a PN-based coordinator", "generally, the same approach could be used for any 'distributed language' you conceive".

Readers and writers

The lecture's second net is the classic readers/writers problem, and the lab asks you to reconstruct it from the slide. The net has places p1 (idle readers/writers), p2 (requesting), p3/p4 (becoming reader/writer), p5 (the resource free), p6 (reading), p7 (writing), with transitions t1..t7; the safety properties are "no more than one writer" and "no readers and writers together", enforced by inhibitor arcs from p6/p7. The same places reappear as numeric variables in the PRISM model of chapter 11, section 6, so keep this net in mind: it is the course's canonical non-trivial model.

8. The modelling stack and the abstraction level of Petri Nets

The lab deck (06-Lab) compresses the whole approach into one picture, with readers/writers as the example at each level:

• Model — a Petri-Net modelling of "readers and writers": a specific system with specific safety properties and a design template;
• Meta-model — Petri Nets: captures parallelism, unbounded size, synchronisation, ... and could be extended;
• Meta-meta-model — transition systems: captures non-deterministic state transition.

The API organisation follows the same three-layer discipline: the syntax of the model is given via a DSL or expressive API; the transition system is compiled from the DSL (states and transition rules); and analysis methods are possibly added, "carefully addressing loops/non-termination/divergence".

The deck's closing methodological note frames modelling as a programming exercise: "Building an abstract model: should first identify key abstractions — namely, the abstraction level; what concepts are key? what need to be neglected? should give them syntax (structure) and semantics (behaviour); it turns out this is essentially a DSL, defining an operational model." And the design side: once the model/DSL is identified, "write down the specification describing your system — this is naturally a design, since it abstracts from implementation details — it is amenable to verification of (some) properties, at least, animation". Finally, bridging the gap: "consider actual (distributed) platform(s) to run the specification — you could turn PNs into actors, tuple spaces, threads, and so on — the desired properties will still hold."

9. Sources of uncertainty: why this is not the end

The lecture ends with the question that motivates the entire rest of Part C. Pervasive computing — IoT, CPS — has two structural sources of complexity that plain transition systems cannot express:

• Openness — systems tend to well accept new users/services/devices; the number of devices tends to increase (also due to miniaturization); devices are heterogeneous (abstraction is needed); the behaviour of interacting humans/agents is not pre-coded.
• Unpredictability — computational events can follow unknown patterns; many devices could fail, and that becomes the normal; the flow of information is subject to delays and losses; humans/agents can only be statistically characterised; the effect of actions can only be estimated.

And here is the critical diagnosis about the tool built in this chapter:

"On the non-determinism modelling mechanism: captures variability of 'outcomes' · does not 'weight' them · does not distinguish what is normal and what exceptional, and neglects performance."

Non-determinism says which outcomes are possible; it cannot say how likely each one is, nor when it happens. That is precisely the gap the next chapter fills: probabilities weight the outcomes (DTMC), rates weight time (CTMC), and stochastic Petri Nets combine both. The transition system of this chapter is the base of the ladder that chapter 10 climbs.

10. Lab: operational steps and R&D directions

The lab repository is https://github.com/mviroli/asmd-public-models (folder u06 on Virtuale), imported in IntelliJ as an SBT project — the same workflow as chapter 6, section 8.

Operational steps

• Step 1 — download and check. Get acquainted with all parts: utils (just the MSet abstraction), modelling (the API/DSL: System, SystemAnalysis as meta-meta-model, then PetriNet as meta-model), examples (extensional SystemChannel; intensional ad-hoc SystemMutualExclusion and by Petri Nets PNMutualExclusion), and test. Check that all Scala tests and checks pass, and understand why each test asserts what it asserts.
• Step 2 — implement readers & writers. Code and analyse the Readers & Writers Petri Net of the slides by cloning PNMutualExclusion — "be sure to be technically excellent". Write good tests: what set of test cases would make you confident in the design? What are the "defining" properties? If you drop the loops (arcs from p6 to p1, and p7 to p1), does "validity" become easier to test/check?
• Step 3 — design a variation. Code and analyse a minimal variation of the Readers & Writers net such that "if a process says it wants to read, it eventually (surely) does so". How would you show evidence that the design is right? Optionally, let an LLM help: what would a (long) prompt be? what would be the role of testing?

R&D tasks

Test your knowledge