[![Build Status][build_img]][ci]
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.
- [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` 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][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`, 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][tla-in-pictures].
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`][doc].
Examples
========
```python
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][cython] module `dd.cudd`
that interfaces to [CUDD][cudd].
Instructions are available [at `dd`][dd].
License
=======
[BSD-3][bsd3], see `LICENSE` file.
[specs]: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf
[synthesis]: https://doi.org/10.1007/BFb0035748
[moore]: https://web.archive.org/web/20120216141113/http://people.mokk.bme.hu/~kornai/termeszetes/moore_1956.pdf
[mealy]: https://doi.org/10.1002/j.1538-7305.1955.tb03788.x
[streett1]: https://doi.org/10.1016/j.ic.2005.01.006
[gr1]: https://doi.org/10.1007/11609773_24
[rabin1]: https://online.tugraz.at/tug_online/voe_main2.getvolltext?pCurrPk=47554
[fol]: https://en.wikipedia.org/wiki/First-order_logic
[past LTL]: https://doi.org/10.1007/3-540-15648-8_16
[LTL]: https://doi.org/10.1109/SFCS.1977.32
[temporal testers]: https://doi.org/10.1007/978-3-540-69850-0_11
[rigid quantification]: https://doi.org/10.1007/978-1-4612-4222-2
[bitblasting]: https://doi.org/10.1007/978-3-540-74105-3
[bdd]: https://doi.org/10.1109/TC.1986.1676819
[tla-in-pictures]: https://doi.org/10.1109/32.464544
[doc]: https://github.com/tulip-control/omega/blob/main/doc/doc.md
[cython]: https://en.wikipedia.org/wiki/Cython
[cudd]: http://vlsi.colorado.edu/~fabio/CUDD
[dd]: https://github.com/tulip-control/dd#cython-bindings
[bsd3]: https://opensource.org/licenses/BSD-3-Clause
[build_img]: https://github.com/tulip-control/omega/actions/workflows/main.yml/badge.svg?branch=main
[ci]: https://github.com/tulip-control/omega/actions
Raw data
{
"_id": null,
"home_page": "https://github.com/tulip-control/omega",
"name": "omega",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.11",
"maintainer_email": "",
"keywords": "first-order,propositional,logic,quantifier,forall,exists,fixpoint,mu-calculus,formula,flatten,bitblaster,bitvector,arithmetic,binary decision diagram,symbolic,games,specification,system,assume,guarantee,satisfiability,enumeration,state machine,transition system,automaton,automata,streett,rabin,temporal logic,temporal tester,gr1,generalized reactivity",
"author": "Caltech Control and Dynamical Systems",
"author_email": "tulip@tulip-control.org",
"download_url": "https://files.pythonhosted.org/packages/14/4e/00f0acb52430c9f04ad526466925d58ba489ae0c9628186e291a5d11cc83/omega-0.4.0.tar.gz",
"platform": null,
"description": "[![Build Status][build_img]][ci]\n\n\nAbout\n=====\n\nA package of symbolic algorithms using binary decision diagrams (BDDs)\nfor synthesizing implementations from [temporal logic specifications][specs].\nThis is useful for designing systems, especially vehicles that carry humans.\n\n\n- [Synthesis][synthesis] algorithms for [Moore][moore] or [Mealy][mealy]\n implementations of:\n\n - [generalized Streett(1)][streett1] specifications (known as [GR(1)][gr1])\n - generalized Rabin(1) specifications ([counter-strategies][rabin1] to GR(1))\n - detection of trivial realizability in GR(1) specifications.\n\n See `omega.games.gr1` and the example `gr1_synthesis_intro`.\n\n\n- Enumeration of state machines (as `networkx` graphs) from the synthesized\n symbolic implementations. See `omega.games.enumeration`.\n\n\n- Facilities to simulate the resulting implementations with little and\n readable user code. See `omega.steps` and the example `moore_moore`.\n\n\n- Code generation for the synthesized *symbolic* implementations.\n This code is correct-by-construction. See `omega.symbolic.codegen`.\n\n\n- *Minimal covering* with a symbolic algorithm to find a minimal cover, and to\n enumerate all minimal covers. Used to convert BDDs to *minimal* formulas.\n See `omega.symbolic.cover` and `omega.symbolic.cover_enum`, and the\n example `minimal_formula_from_bdd`.\n\n\n- [First-order][fol] [linear temporal logic][LTL] (LTL) with\n [rigid quantification][rigid quantification] and substitution.\n See `omega.logic.lexyacc`, `omega.logic.ast`, and `omega.logic.syntax`.\n\n\n- [Bitblaster][bitblasting] of quantified integer arithmetic (integers -> bits).\n See `omega.logic.bitvector`.\n\n\n- Translation from [past][past LTL] to future LTL, using\n [temporal testers][temporal testers]. See `omega.logic.past`.\n\n\n- Symbolic automata that manage first-order formulas by seamlessly using\n [binary decision diagrams][bdd] (BDDs) underneath. You can:\n\n - declare variables and constants\n - translate:\n 1. formulas to BDDs and\n 2. BDDs to *minimal* formulas via minimal covering\n - quantify\n - substitute\n - prime/unprime variables\n - get the support of predicates\n - pick satisfying assignments (or work with iterators)\n - define operators\n\n See `omega.symbolic.temporal` and `omega.symbolic.fol` for more details.\n\n\n- Facilities to write symbolic fixpoint algorithms.\n See `omega.symbolic.fixpoint` and `omega.symbolic.prime`, and the example\n `reachability_solver`.\n\n\n- Conversion from graphs annotated with formulas to temporal logic formulas.\n These graphs can help specify transition relations.\n The translation is in the spirit of\n [predicate-action diagrams][tla-in-pictures].\n\n See `omega.symbolic.logicizer` and `omega.automata` for more details, and\n the example `symbolic`.\n\n\n- Enumeration and plotting of state predicates and actions represented as BDDs.\n See `omega.symbolic.enumeration`.\n\n\nDocumentation\n=============\n\nIn [`doc/doc.md`][doc].\n\n\nExamples\n========\n\n```python\nimport omega.symbolic.fol as _fol\n\nctx = _fol.Context()\nctx.declare(\n x=(0, 10),\n y=(-2, 5),\n z='bool')\nu = ctx.add_expr(\n r'(x <= 2) /\\ (y >= -1)')\nv = ctx.add_expr(\n r'(y <= 3) => (x > 7)')\nr = u & ~ v\nexpr = ctx.to_expr(r)\nprint(expr)\n```\n\n\nInstallation\n============\n\n```\npip install omega\n```\n\nThe package and its dependencies are pure Python.\n\nFor solving demanding games, install the [Cython][cython] module `dd.cudd`\nthat interfaces to [CUDD][cudd].\nInstructions are available [at `dd`][dd].\n\n\nLicense\n=======\n[BSD-3][bsd3], see `LICENSE` file.\n\n\n[specs]: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf\n[synthesis]: https://doi.org/10.1007/BFb0035748\n[moore]: https://web.archive.org/web/20120216141113/http://people.mokk.bme.hu/~kornai/termeszetes/moore_1956.pdf\n[mealy]: https://doi.org/10.1002/j.1538-7305.1955.tb03788.x\n[streett1]: https://doi.org/10.1016/j.ic.2005.01.006\n[gr1]: https://doi.org/10.1007/11609773_24\n[rabin1]: https://online.tugraz.at/tug_online/voe_main2.getvolltext?pCurrPk=47554\n[fol]: https://en.wikipedia.org/wiki/First-order_logic\n[past LTL]: https://doi.org/10.1007/3-540-15648-8_16\n[LTL]: https://doi.org/10.1109/SFCS.1977.32\n[temporal testers]: https://doi.org/10.1007/978-3-540-69850-0_11\n[rigid quantification]: https://doi.org/10.1007/978-1-4612-4222-2\n[bitblasting]: https://doi.org/10.1007/978-3-540-74105-3\n[bdd]: https://doi.org/10.1109/TC.1986.1676819\n[tla-in-pictures]: https://doi.org/10.1109/32.464544\n[doc]: https://github.com/tulip-control/omega/blob/main/doc/doc.md\n[cython]: https://en.wikipedia.org/wiki/Cython\n[cudd]: http://vlsi.colorado.edu/~fabio/CUDD\n[dd]: https://github.com/tulip-control/dd#cython-bindings\n[bsd3]: https://opensource.org/licenses/BSD-3-Clause\n\n[build_img]: https://github.com/tulip-control/omega/actions/workflows/main.yml/badge.svg?branch=main\n[ci]: https://github.com/tulip-control/omega/actions\n",
"bugtrack_url": null,
"license": "BSD",
"summary": "Symbolic algorithms for solving games of infinite duration.",
"version": "0.4.0",
"project_urls": {
"Bug Tracker": "https://github.com/tulip-control/omega/issues",
"Documentation": "https://github.com/tulip-control/omega/blob/main/doc/doc.md",
"Homepage": "https://github.com/tulip-control/omega",
"Source Code": "https://github.com/tulip-control/omega"
},
"split_keywords": [
"first-order",
"propositional",
"logic",
"quantifier",
"forall",
"exists",
"fixpoint",
"mu-calculus",
"formula",
"flatten",
"bitblaster",
"bitvector",
"arithmetic",
"binary decision diagram",
"symbolic",
"games",
"specification",
"system",
"assume",
"guarantee",
"satisfiability",
"enumeration",
"state machine",
"transition system",
"automaton",
"automata",
"streett",
"rabin",
"temporal logic",
"temporal tester",
"gr1",
"generalized reactivity"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "144e00f0acb52430c9f04ad526466925d58ba489ae0c9628186e291a5d11cc83",
"md5": "bdb10473e4b8740a1362d97697f7dcb0",
"sha256": "c705a0d1618e20bd233dbd35e1ab0800c62a42f1b5b9be70af44fae1cd79723f"
},
"downloads": -1,
"filename": "omega-0.4.0.tar.gz",
"has_sig": false,
"md5_digest": "bdb10473e4b8740a1362d97697f7dcb0",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.11",
"size": 208972,
"upload_time": "2024-02-16T15:25:15",
"upload_time_iso_8601": "2024-02-16T15:25:15.627515Z",
"url": "https://files.pythonhosted.org/packages/14/4e/00f0acb52430c9f04ad526466925d58ba489ae0c9628186e291a5d11cc83/omega-0.4.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-02-16 15:25:15",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "tulip-control",
"github_project": "omega",
"travis_ci": false,
"coveralls": false,
"github_actions": true,
"requirements": [],
"lcname": "omega"
}
JSON
