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