Skip to content

Formal Methods

← Back to Domain-Specific Abstractions by Domain

6 domain-specific abstractions whose origin domain is Formal Methods.

  • Abstract state machine — A formal operational model in which each state is an arbitrary mathematical structure and guarded updates define discrete state transitions.
  • Alternating-time temporal logic — A branching-time logic for concurrent games whose coalition modalities assert that selected agents have a strategy to ensure a temporal objective regardless of the other agents' choices.
  • Hidden algebra — An algebraic specification framework for stateful and concurrent systems that distinguishes visible data sorts from hidden state sorts and characterizes state by observable behavior.
  • Petri net — A bipartite place-transition graph with a token marking whose enabled transition firings consume and produce tokens, modeling concurrency, synchronization and resource flow in discrete-event systems.
  • Postcondition — A predicate required to hold immediately after a program operation or specified code region completes normally.
  • Rewriting — Rule-governed replacement of a subexpression by another expression within a formal object.