LTL 控制器综合

模型检查问“这台给定机器的所有运行是否正确”，综合则要选出机器本身。环境输入是不可控制选择，控制器输出是可设计选择；把两种边混成自动机的普通非确定后继，会丢掉存在策略、全称环境的先后顺序。

确定监控器使过去输入输出唯一确定当前q，不需要猜未来。一般LTL先经LTL 到 Büchi 转换公理库LTL 到 Büchi 自动机的转换LTL to Büchi translation · LTL-to-automata translation用闭包、局部一致状态、时序转移与逐个 Until 接受条件，把 LTL 的无限等待义务转换为 Büchi 自动机。取得识别公式本身的非确定自动机；这里不是模型检查中识别否定公式的坏行为机。其接受分支只保证对完整词存在，并不保证能在线选对；因此不能直接把NBA所有分支交给控制器自由选择。Safra确定化公理库Safra 的 Büchi 确定化Safra determinization · Safra tree construction以命名有序树记录非确定Büchi的接受进展，用持续存在且无限变绿的节点构造确定Rabin自动机。及后续接受条件转换是经典可行途径之一，也有其他保持正确策略语义的综合流程。

具体的后续条件转换可先把确定 Rabin 机改写为同图 Muller 条件：允许的集合为所有满足某一对 $S\cap E_i=\varnothing$ 且 $S\cap F_i\ne \varnothing$ 的 $S\subseteq Q$。再用Muller 的 LAR 构造公理库Muller 自动机与最近出现记录Muller automaton · Latest appearance record · LAR construction用最近出现排列记录无限重复状态集合，将确定Muller接受条件转换为带有限记忆的奇偶条件。得到确定奇偶监控器。这是一条有明确输入输出条件的有限流程；显式列举接受族和增加排列记忆的成本都应计入翻译。

请求与可用信号 ​

输入为req、ready，输出为grant。希望满足

没有环境假设时不可实现：环境先发请求，再永远令ready=false。控制器若授权就违反S，若永不授权就违反R。

较弱假设 $A_{req}=G(req\to Fready)$ 已足以使Mealy方案可实现。控制器记一位pending，初始false，每轮令

每个未回应请求让pending保持真；假设保证之后某轮ready，届时grant为真并清账。S无条件成立，R在A_req成立的输入上成立。同一轮req与ready都真时可立即授权，因为F允许当前时刻兑现。

三优先级监控器 ​

为把公平假设做成一个小奇偶图，下面采用更强、形式更简单的 $A=GFready$。规格固定为

这表示安全S始终要守，环境违反公平时只免除响应R。它不同于 $A\to (S\wedge R)$，后者会在不公平环境下连安全也一并免除。

仍用pending更新式，但监控器不替控制器选择grant，而是读取任意联合字母。若grant=true且ready=false，进入永久拒绝状态D。其他情况计算pending′，进入以下状态：

初态Q。在从未进入D的运行中，Q出现无限次等价于没有请求被永久拖欠，因此R成立；若Q只有限出现，就最终一直pending。此时ready无限出现会让P₁无限出现，最小色1拒绝；ready仅有限出现则最终只见P₀的2，表示公平前提失败而响应义务被解除。D的1自环另保证任何一次非法授权都不能被后来不公平“洗掉”。

一段合法策略执行为：输入(req,ready)依次(1,0)、(0,0)、(0,1)，输出grant依次0、0、1，监控器Q→P₀→P₀→Q。之后即使还有任意长但有限的不可用区间，只要GFready成立，每次pending最终仍能被清掉。

为什么Mealy改Moore会改变答案 ​

Moore时序公理库Moore 机Moore machine · Moore automaton把输出标在状态上，并在初态及每次状态更新后观察输出的确定有限状态机器。要求控制器先输出oₜ，再看到本轮iₜ。对同一即时安全条件grant→ready，控制器不能提前知道ready。

环境可以一直req=true，并在控制器第一次grant=true的那一轮令ready=false，其余轮令ready=true。如果控制器从不授权，GFready成立而R失败；若它某轮授权，S立即失败，此后环境持续ready=true仍满足公平。故这个Moore版本不可实现，而刚才的Mealy版本可实现。

把输出解释成“下一轮授权”可以得到另一份有意义的接口，但须同步调整公式中的X及时间对齐。单纯把机器类型名称换掉，不会保留同一个综合问题。

从位置策略提取实现 ​

把四状态监控器按“环境输入、控制器输出”展开，调用Zielonka求解器公理库Zielonka 奇偶博弈算法Zielonka algorithm · Recursive parity game solver按最小优先级吸引域递归求解，在对手种子非空时回原图扩张并二次递归，保留双方位置策略。。Even在每个可达(q,i)挑一条获胜输出边，并按δ更新记忆，就得到有限控制器。该位置策略是对扩展图无记忆，对原始输入接口可能仍需要保存监控状态。

本例还有更简单的合法实现grant=ready，因为规格允许没有请求时也授权。若希望不主动授权，可以选择上面的pending版本；这种约束或偏好没有出现在原公式里时，综合器不会自动替设计者补上。得到一个获胜实现也不等于得到状态数最少、延迟最短的实现。

若初态在Odd获胜区，输出环境反策略比只说“不可实现”更有帮助。反策略必须尊重环境在回合中能看到的信息，并用真实输入迫使安全违例或长期未回应，不能用一条控制器本可避开的失败路径冒充证书。

把展开图交给只记录端点关系的奇偶求解器时，可合并同一 $(q,i)$ 到同一后继的平行输出边，但要为每个保留后继存一个产生它的输出 $o$。位置策略选中的是后继顶点，再由这份见证恢复输出；若多个输出给出同一监控后继，任选一个已记录的见证即可。动作标记版本则直接保留各条输出边。两种表示的获胜区相同，边数与控制器提取的账本却不能混用。

构造成本与规格边界 ​

若确定监控器有N个状态、输入/输出字母数分别为a、b，直接展开有N(1+a)个顶点、Na(1+b)条带动作边，之后还需支付奇偶求解和策略输出成本。a=2^|I|、b=2^|O|时，显式字母枚举本身就可能昂贵，符号表示需另行分析。

一般 LTL 有双指数规模的标准确定自动机翻译，且最坏情况确需这一量级，不能用本例四状态监控器代表普遍成本。上面把整台确定 Rabin 机显式改写为 Muller 再做 LAR 的流程，只提供透明的存在性构造，不承诺达到这个最优规模界：若中间已有 N 个状态，LAR 的 N! 记忆可能再增加一层指数。要获得标准双指数界，应使用保留较小接受对结构的转换或直接确定奇偶构造。朴素 Zielonka 的宽松指数上界也不能忽略；应分别报告所选规格翻译、积图与实际求解方法。

单元终点给出完整16顶点展开及递归获胜证书，再比较禁止授权的接口和Moore接口，要求交付真实控制器或环境反策略，并核对假设失效时哪些义务仍然保留。