Abstract: Static [k] resiliency is concerned with the ability for workflows to recover executing from exceptions of resource unavailability. To verify it, up to [C(|U|,k)] Workflow Satisfiability（WS） decision problems should be solved（where [U] is the set of all resources） and the corresponding costs are huge. In existing work, one WS counting problem is solved to quantify the ability of a workflow to recover from exceptions. However, this indicator is somewhat rough, and only in the case of no satisfiability solution an accurate negative conclusion can be given. In this paper, for an exclusion and binding constrained workflow, a novel model which surrounds the concept of satisfiability counting lower bound of static [k] resiliency is established, and such a no-trivial lower bound is proved for the first time. Therefore, the negative condition of [k] resiliency is generalized, from unsatisfiable cases to satisfiable ones. This result has representative meanings in theory, by which the precisely applied range of the aforesaid indicator is also extended.

Key words: workflow, authorization, constraint, resource allocation, resiliency, satisfiability

摘要： 静态[k]弹性反映安全工作流从资源失效异常中恢复运行的能力，但其验证须求解多达[C(|U|,k)]个工作流可满足决策问题（[U]为资源集），代价巨大。已有工作提出通过1次工作流可满足计数来量化其异常恢复能力，但该指标相当粗糙，仅能在可满足无解情形下给出精确的否定结论。对互斥和绑定约束下的工作流，建立了以[k]弹性可满足计数下界概念为核心的新颖模型，并首次证明了一个非平凡的下界，由此可将[k]弹性的否决条件从可满足无解推广到有解情形，具有理论上的代表性意义，也扩大了前述指标精确适用的范围。

关键词: 工作流, 授权, 约束, 资源分配, 弹性, 可满足性