libomega

libomega is a Rust library for finite omega automata. It provides compact indexed models, seven state-based acceptance families, bounded conversions to Büchi form, Büchi-language emptiness decisions, omega-language closure and relation decisions, and independent local checking of the resulting mathematical evidence. It also provides finite parity games, exact fairness compilation, positional strategies, and independently checked progress measures.

The library is designed as an in-process semantic kernel for model checkers and static analyzers such as cpgmc. Callers retain responsibility for parsing source languages, selecting abstractions, attaching source identities, caching, and continuous-integration policy. libomega receives typed values and returns typed outcomes; it does not define storage or transport formats.

Implemented capabilities

• Dense, compact state and symbol domains with canonical transition relations.
• Büchi, generalized Büchi, co-Büchi, minimum-recurring-even parity, Rabin, Streett, and Muller acceptance.
• Exact, bounded conversion of every supported acceptance family to Büchi form.
• Exact finite Büchi emptiness decisions using ranked proofs or accepting lassos.
• Same-alphabet union and intersection, total symbol projection, and exact deterministic-complete complement profiles.
• Exact inclusion and equivalence where complement is supported, plus sufficient direct simulation and bisimulation certificates.
• Deterministic parity-game solving with complete Even/Odd winning partitions, positional strategies, and original/dual progress measures.
• Exact Büchi, co-Büchi, and generalized-Büchi justice compilation to parity, including explicit finite strategy memory.
• Independently implemented checkers for Büchi evidence and conversion evidence.
• Independent parity-game checking of exact content binding, partitions, strategies, measures, and local progress obligations.
• Deterministic resource admission, checked arithmetic, fallible allocation, and iterative traversal throughout subject-dependent algorithms.
• Closed formal-to-source invariant traceability and derived property plans.

Library example

The stable facade groups the public API by responsibility:

use libomega::automata::{
    IndexedBuchiBuilder, IndexedBuchiInput, IndexedBuildLimits, TransitionInput,
};
use libomega::buchi::{IndexedBuchiLimits, decide_buchi_emptiness};
use libomega::evidence::EvidenceConclusion;

fn main() -> Result<(), Box<dyn std::error::Error>> {
    let transitions = [
        TransitionInput::new(0, 0, 1),
        TransitionInput::new(1, 0, 1),
    ];
    let built = IndexedBuchiBuilder::new(
        IndexedBuchiInput {
            state_count: 2,
            symbol_count: 1,
            initial_states: &[0],
            accepting_states: &[1],
            transitions: &transitions,
        },
        IndexedBuildLimits {
            max_states: 2,
            max_symbols: 1,
            max_input_transitions: 2,
            max_input_state_memberships: 2,
            max_output_bytes: 4_096,
            max_working_bytes: 8_192,
        },
    )
    .build()?;

    let decision = decide_buchi_emptiness(
        built.automaton().as_view(),
        IndexedBuchiLimits::default(),
    )?;
    assert_eq!(decision.conclusion(), EvidenceConclusion::Refuted);
    Ok(())
}

Complete, compiled examples are buchi.rs and acceptance.rs, and relations.rs, and games.rs.

Architecture

The facade depends on six focused libraries:

Library	Responsibility
libomega-core	Compact validated models, acceptance values, and typed identifiers
libomega-evidence	Allocation-free checking of Büchi proof and witness candidates
libomega-buchi	Bounded iterative search and canonical evidence production
libomega-acceptance	Bounded acceptance products and an independent conversion checker
libomega-relations	Bounded closure, exact language decisions, simulations, and local relation checking
libomega-games	Bounded parity games, exact fairness products, strategies, and local game checking

The search procedures do not grant authority to their own output. A Proved or Refuted result is returned only after a separate checker validates every local obligation against the supplied model. Resource exhaustion is Incomplete; malformed evidence or an internal inconsistency is an error.

Documentation

The documentation map links the theory, scientific qualification method, architecture, design rationale, engineering contracts, security model, usage guide, and API reference. The mathematical starting point is omega-automata semantics, and the concrete integration path is library usage. The relation algorithms and their exactness boundary are derived in omega-language relations. Parity-game semantics and implementation are covered by finite parity games and parity-game solving.

Verification

The aggregate verifier is memory-bounded by the repository wrapper:

./scripts/verify.sh

It checks diagrams, documentation, invariant traceability, formal property plans, formal models, formatting, strict linting, tests, architectural boundaries, constrained-stack behavior, fuzzing, mutation adequacy, and byte-reproducible library packages. See formal verification and qualification for the evidence model.

License

Licensed under the Apache License, Version 2.0.