
Research
Security News
The Growing Risk of Malicious Browser Extensions
Socket researchers uncover how browser extensions in trusted stores are used to hijack sessions, redirect traffic, and manipulate user behavior.
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:
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:
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
.
In doc/doc.md
.
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)
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
.
BSD-3, see LICENSE
file.
FAQs
Symbolic algorithms for solving games of infinite duration.
We found that omega demonstrated a healthy version release cadence and project activity because the last version was released less than a year ago. It has 3 open source maintainers collaborating on the project.
Did you know?
Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.
Research
Security News
Socket researchers uncover how browser extensions in trusted stores are used to hijack sessions, redirect traffic, and manipulate user behavior.
Research
Security News
An in-depth analysis of credential stealers, crypto drainers, cryptojackers, and clipboard hijackers abusing open source package registries to compromise Web3 development environments.
Security News
pnpm 10.12.1 introduces a global virtual store for faster installs and new options for managing dependencies with version catalogs.