Constraint-Driven Synthesis of Hyper Petri Nets
- URL: http://arxiv.org/abs/2607.22062v1
- Date: Fri, 24 Jul 2026 07:57:19 GMT
- Title: Constraint-Driven Synthesis of Hyper Petri Nets
- Abstract summary: This paper addresses the modeling and synthesis of constrained robotic system behaviors using Petri nets (PNs)<n>It investigates how to construct models in which all observable system states satisfy given logical constraints while remaining consistent with executable transition semantics.<n>The proposed method introduces an explicit execution semantics over observable states, induced by admissible (atomic) firing sequences.
- Score: 46.9047309711542
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This paper addresses the modeling and synthesis of constrained robotic system behaviors using Petri nets (PNs). It investigates how to construct models in which all observable system states satisfy given logical constraints while remaining consistent with executable transition semantics. To answer this, we introduce the Hyper Petri Net (HyPN) approach, which synthesizes Petri nets from Boolean specifications while explicitly distinguishing between observable markings and underlying Petri net execution. The proposed method introduces an explicit execution semantics over observable states, induced by admissible (atomic) firing sequences, ensuring by construction that all observable markings satisfy the constraints and revealing a fundamental mismatch between logical feasibility and executable behavior. This is demonstrated in two scenarios inspired by a lunar rover system. These results are particularly relevant for the design of robotic and autonomous systems, as they provide a structured way to ensure correct system configurations while explicitly accounting for execution constraints. The proposed framework further suggests new research directions in execution abstraction, admissible transition systems, and policy selection for navigating between constraint-satisfying states.
Related papers
- Replicating Belief, Not Bits: Epistemic State Replication for Agentic Systems [2.124730017640531]
In distributed systems, the classical State Machine Replication model assumes that correct replicas execute deterministic transitions to yield identical bitwise states.<n>We propose Epistemic State Replication (ESR), a belief-replication layer for agentic distributed systems that shifts the replication boundary from data visibility to knowledge visibility.
arXiv Detail & Related papers (2026-07-03T19:59:03Z) - Steered Generation via Gradient-Based Optimization on Sparse Query Features [1.587869707099313]
Prototype-Based Sparse Steering is a framework that applies Sparse Autoencoders specifically to query activations.<n>We demonstrate that sparse query representations provide the necessary disentanglement for unified, interpretable control over both logical planning and stylistic nuance.
arXiv Detail & Related papers (2026-05-21T21:13:14Z) - CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
Virtual Cell Modeling (VCM) requires models that not only predict perturbation responses, but also support targeted revision when predictions fail.<n>Current LLM-assisted modeling face a refinement-routing problem: prediction discrepancies are observed through executable implementations.<n>We propose CellScientist, a dual-space hierarchical framework that couples a high-level hypothesis space with a low-level executable implementation space.
arXiv Detail & Related papers (2026-05-08T06:40:24Z) - Ontology-Aware Design Patterns for Clinical AI Systems: Translating Reification Theory into Software Architecture [0.0]
Clinical AI systems routinely train on health data structurally distorted by documentation, billing incentives, and terminology fragmentation.<n>This paper proposes seven-aware design patterns in Gang-of-Four pattern language for building clinical AI pipelines resilient to ontological distortion.
arXiv Detail & Related papers (2026-04-02T06:05:11Z) - Behavior Trees vs Executable Ontologies: a Comparative Analysis of Robot Control Paradigms [51.56484100374058]
We compare two approaches to modeling robotic behavior: imperative Behavior Trees (BTs) and declarative Executable Ontologies (EO)<n>BTs structure behavior hierarchically using control-flow, whereas EO represents the domain as a temporal, event-based semantic graph driven by dataflow rules.
arXiv Detail & Related papers (2025-11-19T09:38:01Z) - AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
arXiv Detail & Related papers (2025-07-06T08:35:22Z) - A Constructive Framework for Nondeterministic Automata via Time-Shared, Depth-Unrolled Feedforward Networks [0.0]
We present a formal and constructive simulation framework for nondeterministic finite automata (NFAs) using time-shared, depth-unrolled feedforward networks (TS-FFNs)<n>Our formulation symbolically encodes automaton states as binary vectors, transitions as sparse matrix transformations, and nondeterministic branching-including $varepsilon$-closures-as compositions of shared thresholded updates.
arXiv Detail & Related papers (2025-05-30T01:18:35Z) - Pretrained Embeddings as a Behavior Specification Mechanism [17.86560073144763]
We introduce embeddings as a first-class construct in a specification language.<n>We show that embedding-based specifications can be used to steer a system towards desirable behaviors.
arXiv Detail & Related papers (2025-03-03T19:41:22Z) - Bisimulation Learning [55.859538562698496]
We compute finite bisimulations of state transition systems with large, possibly infinite state space.
Our technique yields faster verification results than alternative state-of-the-art tools in practice.
arXiv Detail & Related papers (2024-05-24T17:11:27Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
We propose a method for synthesising controllers for Markov jump linear systems.
Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS.
We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
arXiv Detail & Related papers (2022-12-01T17:36:30Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.