离散时间相位Petri盒演算dtphPBC
Discrete time phased Petri box calculus dtphPBC
AI总结：
研究提出离散时间相位Petri盒演算dtphPBC，是dtsdPBC的扩展，通过有限吸收DTMC的TPM指定多动作延迟，利用标记概率转移系统及SOS规则构建操作语义，示例展示了动态表达式转移系统的构建方法。
AI中文摘要：
我们提出了离散时间相位Petri盒演算（dtphPBC），它是I.V. Tarasyuk之前提出的离散时间随机和确定性Petri盒演算（dtsdPBC）的扩展，具有相位类型分布的多动作延迟。在dtphPBC中，具有单个吸收状态的有限吸收离散时间马尔可夫链（DTMC）的转移概率矩阵（TPM）指定了相位多动作的离散相位类型（DPH）分布延迟。正相位（定时）多动作具有由非空TPM矩阵表示的正DPH延迟，零相位（即时）多动作具有由空瞬态TPM表示的零DPH延迟。dtphPBC的步操作语义通过标记概率转移系统构建。通过结构操作语义（SOS）规则，转移系统纳入了执行的相位多动作的DPH延迟的吸收DTMC。SOS规则在吸收DTMC的瞬态状态之间的转移以及其吸收状态的自环上定义了空集标记。从瞬态状态（正相位）到吸收状态（零相位）的转移用执行标记，即正相位标记的定时多动作，其（正）延迟由吸收DTMC定义。一系列示例展示了如何构建由定时和即时多动作与演算的不同操作组合而成的动态表达式的转移系统。
英文摘要：
We propose discrete time phased Petri box calculus (dtphPBC), an extension with phase type distributed multiaction delays of discrete time stochastic and deterministic Petri box calculus (dtsdPBC), previously presented by I.V. Tarasyuk. In dtphPBC, transition probability matrices (TPMs) of finite absorbing discrete time Markov chains (DTMCs) with a single absorbing state specify discrete phase type (DPH) distributed delays (including zero delay) of the phased multiactions that generalize stochastic and deterministic multiactions from dtsdPBC. The positively phased (timed) multiactions have positive DPH delays represented by the non-empty TPM matrices over transient states (transient TPMs). The zero phased (immediate) multiactions have zero DPH delay represented by the empty transient TPM. The step operational semantics of dtphPBC is constructed via labeled probabilistic transition systems. The transition systems incorporate the absorbing DTMCs of the DPH delays of the executed phased multiactions via the structural operational semantics (SOS) rules. The SOS rules define a labeling with the empty set on the transitions among transient states of the absorbing DTMC and on the self-loop in the absorbing state of it. The transitions going from the transient states (positive phases) to the absorbing state (zero phase) are labeled with the executions, being the positive phases-superscribed timed multiactions whose (positive) delays are defined by the absorbing DTMC. A series of examples demonstrates how to construct the transition systems of the dynamic expressions, combined from timed and immediate multiactions with different operations of the calculus.
