From diagnosis of active systems to incremental determinization of finite acyclic automata

Abstract

A non-functional requirement for model-based diagnosis of active systems is efficient determinization of acyclic automata. In literature, determinization of finite automata is performed by the Subset Construction algorithm (SC): given a nondeterministic automaton 𝒩, an equivalent deterministic automaton 𝒟 is generated, with each state in 𝒟 being a subset of states in 𝒩. However, SC is conceived for monolithic determinization, when 𝒩 is completely specified. By contrast, monitoring-based diagnosis of active systems requires incremental determinization. We consider the Incremental Determinization Problem for finite acyclic automata: after extending the acyclic automaton 𝒩 to 𝒩′ by Δ𝒩 (by new transitions and, possibly, new states), we require 𝒩′ to be determinized into 𝒟′ based on 𝒟 and Δ𝒩. Although this problem can be naively solved by applying SC to 𝒩′ (thereby disregarding both 𝒟 and Δ𝒩), this solution is bound to lead to poor performances, as it does not exploit the incremental nature of 𝒩′. Therefore, an incremental algorithm is proposed, called ISCA, which extends 𝒟 into 𝒟′ based on Δ𝒩, rather than starting from scratch the determinization of 𝒩′. ISCA is a general-purpose algorithm. Evidence from experiments indicates that, in time, ISCA is significantly more efficient than SC in solving incremental determinization problems.