Formal Foundations for Controlled Stochastic Activity Networks

TL;DR

This paper introduces Controlled Stochastic Activity Networks, a formal framework that integrates control actions with stochastic timing and nondeterminism, enabling rigorous modeling and analysis of complex real-time systems under uncertainty.

Contribution

It extends classical Stochastic Activity Networks with explicit control, providing a unified semantic framework, formal policy taxonomy, and behavioral equivalences for system verification.

Findings

Developed hierarchical automata-theoretic semantics for Controlled SANs.

Formalized a taxonomy of control policies with expressive power characterization.

Introduced behavioral equivalences for model abstraction and reasoning.

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.