Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formal Foundations for Controlled Stochastic Activity Networks

Ali Movaghar

TL;DR

This work introduces Controlled SANs, an automata-based formalism that unifies control actions, nondeterminism, probability, and stochastic timing for modeling distributed real-time systems under uncertainty. It develops a layered semantics—nondeterministic, probabilistic, and stochastic—along with a comprehensive policy taxonomy (from memoryless to tape-augmented) and bisimulation notions to enable compositional reasoning and model reduction. The authors characterize expressive power through language hierarchies on finite and infinite words, establish closure properties, and connect Controlled SANs to classical models such as CTMDPs and GSMPs, enabling synthesis and verification within a rigorous framework. The framework also lays groundwork for integrating PAC-based learning and AI-driven control with formal guarantees, offering a principled path toward dependable, decision-aware systems in safety-critical domains.

Abstract

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.

Formal Foundations for Controlled Stochastic Activity Networks

TL;DR

This work introduces Controlled SANs, an automata-based formalism that unifies control actions, nondeterminism, probability, and stochastic timing for modeling distributed real-time systems under uncertainty. It develops a layered semantics—nondeterministic, probabilistic, and stochastic—along with a comprehensive policy taxonomy (from memoryless to tape-augmented) and bisimulation notions to enable compositional reasoning and model reduction. The authors characterize expressive power through language hierarchies on finite and infinite words, establish closure properties, and connect Controlled SANs to classical models such as CTMDPs and GSMPs, enabling synthesis and verification within a rigorous framework. The framework also lays groundwork for integrating PAC-based learning and AI-driven control with formal guarantees, offering a principled path toward dependable, decision-aware systems in safety-critical domains.

Abstract

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.

Paper Structure

This paper contains 7 sections, 55 theorems, 116 equations, 4 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Nondeterministic Models
  4. Probabilistic Models
  5. Stochastic Models
  6. Conclusion
  7. Proofs

Key Result

Proposition 3.6

Let $\mathcal{E_S}$ denote a relation on the set of all controlled automata such that $(S_1, S_2) \in \mathcal{E_S}$ if and only if $S_1$ and $S_2$ are equivalent controlled automata in the sense of Definition def3.5. Then $\mathcal{E_S}$ will be an equivalence relation.

Figures (4)

  • Figure 1: An example of a simple controlled activity network with a marking.
  • Figure 2: Marking of the model after $T1$ completes via control action $c1$ in the model of Figure 1.
  • Figure 3: Marking of the model after $I2$ completes in the model of Figure 2.
  • Figure 4: Marking of the model after $I1$ completes in the model of Figure 3.

Theorems & Definitions (170)

  • Remark 2.1
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Definition 3.5
  • Proposition 3.6
  • Proposition 3.7
  • Definition 3.8
  • Definition 3.9
  • ...and 160 more