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.

翻译：本文提出受控随机活动网络（Controlled SANs），作为经典随机活动网络的形式化扩展，通过将显式控制动作集成到统一语义框架中，用于分布式实时系统建模。受控随机活动网络系统化地捕捉涉及非确定性、概率分支与随机时序的动态行为，同时在严格数学框架内支持策略驱动的决策机制。我们为受控随机活动网络建立了层次化的自动机理论语义，以统一方式涵盖非确定性、概率性与随机性模型。通过形式化定义从无记忆策略、有限记忆策略到计算增强策略的结构化控制策略分类体系，并借助相关语言类别刻画其表达能力。为支持模型抽象与组合推理，我们引入了行为等价关系，包括互模拟与随机同构。受控随机活动网络推广了连续时间马尔可夫决策过程（CTMDPs）等经典框架，为不确定性环境下可靠系统的规约、验证与综合奠定了严格的理论基础。该框架支持定量与定性分析，推动了控制逻辑、时序约束与随机性紧密耦合的安全关键系统设计方法的发展。