Symbolic algorithms for solving games of infinite duration.
Project description
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 (counterstrategies to GR(1))
 detection of trivial realizability in GR(1) specifications.
See
omega.games.gr1
and the examplegr1_synthesis_intro
. 
Enumeration of state machines (as
networkx
graphs) from the synthesized symbolic implementations. Seeomega.games.enumeration
. 
Facilities to simulate the resulting implementations with little and readable user code. See
omega.steps
and the examplemoore_moore
. 
Code generation for the synthesized symbolic implementations. This code is correctbyconstruction. 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
andomega.symbolic.cover_enum
, and the exampleminimal_formula_from_bdd
. 
Firstorder linear temporal logic (LTL) with rigid quantification and substitution. See
omega.logic.lexyacc
,omega.logic.ast
, andomega.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 firstorder formulas by seamlessly using binary decision diagrams (BDDs) underneath. You can:
 declare variables and constants
 translate:
 formulas to BDDs and
 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
andomega.symbolic.fol
for more details. 
Facilities to write symbolic fixpoint algorithms. See
omega.symbolic.fixpoint
andomega.symbolic.prime
, and the examplereachability_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 predicateaction diagrams.
See
omega.symbolic.logicizer
andomega.automata
for more details, and the examplesymbolic
. 
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
BSD3, see LICENSE
file.
Project details
Release history Release notifications  RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.