About

A package of symbolic algorithms using binary decision diagrams (BDDs) for synthesizing implementations from temporal logic specifications. This is useful for designing systems, especially vehicles that carry humans.

• Synthesis algorithms for Moore or Mealy implementations of:

  • generalized Streett(1) specifications (known as GR(1))
  • generalized Rabin(1) specifications (counter-strategies to GR(1))
  • detection of trivial realizability in GR(1) specifications.

  See omega.games.gr1 and the example gr1_synthesis_intro.

• Enumeration of state machines (as networkx graphs) from the synthesized symbolic implementations. See omega.games.enumeration.

• Facilities to simulate the resulting implementations with little and readable user code. See omega.steps and the example moore_moore.

• Code generation for the synthesized symbolic implementations. This code is correct-by-construction. See omega.symbolic.codegen.

• Minimal covering with a symbolic algorithm to find a minimal cover, and to enumerate all minimal covers. Used to convert BDDs to minimal formulas. See omega.symbolic.cover and omega.symbolic.cover_enum, and the example minimal_formula_from_bdd.

• First-order linear temporal logic (LTL) with rigid quantification and substitution. See omega.logic.lexyacc, omega.logic.ast, and omega.logic.syntax.

• Bitblaster of quantified integer arithmetic (integers -> bits). See omega.logic.bitvector.

• Translation from past to future LTL, using temporal testers. See omega.logic.past.

• Symbolic automata that manage first-order formulas by seamlessly using binary decision diagrams (BDDs) underneath. You can:

  • declare variables and constants
  • translate:
    1. formulas to BDDs and
    2. BDDs to minimal formulas via minimal covering
  • quantify
  • substitute
  • prime/unprime variables
  • get the support of predicates
  • pick satisfying assignments (or work with iterators)
  • define operators

  See omega.symbolic.temporal and omega.symbolic.fol for more details.

• Facilities to write symbolic fixpoint algorithms. See omega.symbolic.fixpoint and omega.symbolic.prime, and the example reachability_solver.

• Conversion from graphs annotated with formulas to temporal logic formulas. These graphs can help specify transition relations. The translation is in the spirit of predicate-action diagrams.

  See omega.symbolic.logicizer and omega.automata for more details, and the example symbolic.

• Enumeration and plotting of state predicates and actions represented as BDDs. See omega.symbolic.enumeration.

Documentation

In doc/doc.md.

Examples

import omega.symbolic.fol as _fol

ctx = _fol.Context()
ctx.declare(
    x=(0, 10),
    y=(-2, 5),
    z='bool')
u = ctx.add_expr(
    r'(x <= 2) /\ (y >= -1)')
v = ctx.add_expr(
    r'(y <= 3) => (x > 7)')
r = u & ~ v
expr = ctx.to_expr(r)
print(expr)

Installation

pip install omega

The package and its dependencies are pure Python.

For solving demanding games, install the Cython module dd.cudd that interfaces to CUDD. Instructions are available at dd.

License

BSD-3, see LICENSE file.