Skip to main content

Symbolic algorithms for solving games of infinite duration.

Project description

[![Build Status][build_img]][travis] [![Coverage Status][coverage]][coveralls]

About

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

Features

  • [Synthesis][synthesis] algorithms for [Moore][moore] or [Mealy][mealy] implementations of:

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

    See omega.games.gr1.

  • 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.

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

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

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

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

  • Symbolic automata that manage first-order formulas by seamlessly using [binary decision diagrams][bdd] (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.

  • 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][tla-in-pictures].

    See omega.symbolic.logicizer and omega.automata for more details.

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

Documentation

In [doc/doc.md][doc].

Installation

` pip install omega `

or

` python setup.py install `

The package and its dependencies are pure Python.

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

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Filename, size & hash SHA256 hash help File type Python version Upload date
omega-0.1.2.tar.gz (184.6 kB) Copy SHA256 hash SHA256 Source None

Supported by

Elastic Elastic Search Pingdom Pingdom Monitoring Google Google BigQuery Sentry Sentry Error logging AWS AWS Cloud computing DataDog DataDog Monitoring Fastly Fastly CDN SignalFx SignalFx Supporter DigiCert DigiCert EV certificate StatusPage StatusPage Status page