Formal Foundations for Controlled Stochastic Activity Networks

Fuente: arXiv
Gespeichert in:
Bibliographische Detailangaben
1. Verfasser: Movaghar, Ali
Format: Preprint
Veröffentlicht: 2025
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1866918326416965632
author Movaghar, Ali
author_facet Movaghar, Ali
contents We introduce Controlled Stochastic Activity Networks (Controlled SANs), a formal extension of classical Stochastic Activity Networks that integrates explicit control actions into a unified semantic framework for modeling distributed real-time systems. Controlled SANs systematically capture dynamic behavior involving nondeterminism, probabilistic branching, and stochastic timing, while enabling policy-driven decision-making within a rigorous mathematical framework. We develop a hierarchical, automata-theoretic semantics for Controlled SANs that encompasses nondeterministic, probabilistic, and stochastic models in a uniform manner. A structured taxonomy of control policies, ranging from memoryless and finite-memory strategies to computationally augmented policies, is formalized, and their expressive power is characterized through associated language classes. To support model abstraction and compositional reasoning, we introduce behavioral equivalences, including bisimulation and stochastic isomorphism. Controlled SANs generalize classical frameworks such as continuous-time Markov decision processes (CTMDPs), providing a rigorous foundation for the specification, verification, and synthesis of dependable systems operating under uncertainty. This framework enables both quantitative and qualitative analysis, advancing the design of safety-critical systems where control, timing, and stochasticity are tightly coupled.
format Preprint
id arxiv_https___arxiv_org_abs_2511_12974
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Formal Foundations for Controlled Stochastic Activity Networks
Movaghar, Ali
Formal Languages and Automata Theory
Logic in Computer Science
68Q45, 68Q87, 60J25, 60J27 68Q45, 68Q87, 60J25, 60J27 68Q45, 68Q87, 60J25, 60J27
F.1.1; F.3.1; G.3; I.2.8
We introduce Controlled Stochastic Activity Networks (Controlled SANs), a formal extension of classical Stochastic Activity Networks that integrates explicit control actions into a unified semantic framework for modeling distributed real-time systems. Controlled SANs systematically capture dynamic behavior involving nondeterminism, probabilistic branching, and stochastic timing, while enabling policy-driven decision-making within a rigorous mathematical framework. We develop a hierarchical, automata-theoretic semantics for Controlled SANs that encompasses nondeterministic, probabilistic, and stochastic models in a uniform manner. A structured taxonomy of control policies, ranging from memoryless and finite-memory strategies to computationally augmented policies, is formalized, and their expressive power is characterized through associated language classes. To support model abstraction and compositional reasoning, we introduce behavioral equivalences, including bisimulation and stochastic isomorphism. Controlled SANs generalize classical frameworks such as continuous-time Markov decision processes (CTMDPs), providing a rigorous foundation for the specification, verification, and synthesis of dependable systems operating under uncertainty. This framework enables both quantitative and qualitative analysis, advancing the design of safety-critical systems where control, timing, and stochasticity are tightly coupled.
title Formal Foundations for Controlled Stochastic Activity Networks
topic Formal Languages and Automata Theory
Logic in Computer Science
68Q45, 68Q87, 60J25, 60J27 68Q45, 68Q87, 60J25, 60J27 68Q45, 68Q87, 60J25, 60J27
F.1.1; F.3.1; G.3; I.2.8
url https://arxiv.org/abs/2511.12974