The cascade product is a method for combining two automata in which the first automaton reads symbols from an alphabet Σ, while the second automaton reads symbols from the Cartesian product of Σ and the set of states of the first automaton. This capability of the second automaton to process not only input symbols but also the current state of the first automaton has made the cascade product a fundamental tool in theoretical computer science, with the most notable result being the Krohn-Rhodes Cascade Decomposition Theorem. In this paper, we propose the use of the cascade product in the context of formal verification, specifically for safety model checking. We show that specifying the undesired behaviors of a system through a cascade of automata enables an approach to model checking that is incremental with respect to the specification , where verification proceeds component by component, potentially reusing information obtained from the verification of previous steps. We also demonstrate how to represent a cascade of automata symbolically, thereby making it possible to perform symbolic verification of such properties. A proof-of-concept on a set of simple models, evaluated experimentally, indicates that this approach is promising.
The concept of the cascade product 1 ∘ 2 of two automata 1 and 2 is a fundamental notion in
theoretical computer science [
A fundamental result concerning cascades of automata is the Krohn–Rhodes Cascade Decomposition
Theorem [
In this paper, we investigate the problem of safety model checking [
First (Section 3), we demonstrate that expressing the undesired behaviors of a system through a cascade 1 ∘ 2 ∘ · · · ∘ enables safety model checking to be performed incrementally with respect to 7th International Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis (OVERLAY 2025), October 26, 2025, Bologna, Italy $ luca.geatti@uniud.it (L. Geatti) https://users.dimi.uniud.it/~luca.geatti/ (L. Geatti) 0000-0002-7125-787X (L. Geatti)
© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
1It is worth pointing out that the class of counter-free (semi)automata corresponds to the class of languages definable in
Linear Temporal Logic (LTL,[
Second (Section 4), we present a symbolic modeling for automata cascades, in which the cascade is
represented not through memory locations and pointers, but rather via Boolean formulas [
In Section 5, we present a proof-of-concept in which model checking of cascades of automata is applied to simple system models. The results obtained are promising and suggest the potential of this novel approach.
An automaton is a tuple (Σ, , , 0, ) such that: (i) Σ is a (finite) alphabet; (ii) is a finite set of states; (iii) : × Σ → is a transition function; (iv) 0 ∈ is the initial state; and (v) ⊆ is the set of final states. We say that is two-state if || = 2.
Given an automaton = (Σ, , , 0, ) and a (finite) word := ⟨ 0, . . . , ⟩ ∈ Σ* , we say that is accepted by if reaches a final state reading . We define the language of , denoted by ℒ(), as the set of words accepted by .
The cascade product of automata is defined as follows.
Definition 1 (Cascade product of automata [
′′((, ′), ) = ( (, ), ′(′, (, )))
Fig. 1 shows the cascade product of two automata defining the language · Σ* . We will often simply use “cascade” for “cascade product”. We define the height of the cascade 1 ∘ · · · ∘ as .
Two classes of automata are particularly important in the context of cascades, namely reset and permutation-reset automata, which are defined in terms of the form of their transitions, as follows. Definition 2 (Reset and permutation functions). Let = (Σ, , , 0, ) be an automaton. For each ∈ Σ, we define the function induced by in , denoted by , as the transformation : → such that, for all ∈ , it holds () = ′ if (, ) = ′. We say that is a reset function if there exists ′ ∈ such that () = ′, for all ∈ . In this case, we say that is a reset on ′. If : → is a bijection, then it is called a permutation.
The following classes of automata are defined with respect to the functions induced by the symbols
in their alphabets [
Model checking [13, 14, 15] is an automatic and exhaustive verification technique used to determine whether all executions of a system model–typically represented as a transition system–satisfy a given logical specification, which is usually formulated in temporal logics or via automata.
A transition system is a tuple (Σ, , , ) such that: (i) Σ is a finite alphabet; (ii) is a set of states; (iii) ⊆ × Σ × is the transition relation; (iv) ⊆ is the set of initial states. We define the language of , denoted by ℒ( ), as the set of all its finite computations, i.e., finite sequences ⟨(0, 0), (1, 1), . . .⟩ ∈ ( × Σ)+ that start in initial state 0 ∈ and respect the transition relation . We say that is symbolically represented when is described with Boolean formulas (or SMT formulas, when is infinite). In this case, = (Σ, , (, Σ, ′), ()), where: (i) is a set of state variables and ′ := {′ | ∈ }; (ii) (, Σ, ′) is the formula encoding the transition relation of ; and (iii) () is the formula encoding the initial states of . In this case, we say that is a symbolic transition system.
Below, we present the classical definition of safety model checking of a transition system = (Σ, , , ). Here, the specification consists of a language ℒ ⊆ ( × Σ)+ of finite words, each representing an undesidered behavior that the system should avoid.
Definition 3 (Safety Model Checking). Let = (Σ, , , ) be a transition system and let ℒ ⊆ (× Σ)+. The model checking problem of with respect to ℒ is the problem of establishing whether ℒ( ) ∩ ℒ = ∅.
If ℒ( ) ∩ ℒ ̸= ∅, then the system is deemed unsafe with respect to ℒ, as it admits at least
one computation that is undesired, i.e., belonging to ℒ. It is important to emphasize that this does
not correspond to model checking over finite traces ( e.g., as studied in [16]). Instead, it exactly aligns
with the Safety Model Checking problem (also referred to as the Invariant Checking problem) studied
in [
The above definition is often referred to as explicit-state model checking, meaning that all states of are represeted as memory locations and transitions are implemented as pointers. With the term symbolic model checking, we refer to the same problem in the case is a symbolic transition system.
In this section, we illustrate how specifying the property by means of an automata cascade 1 ∘ · · · ∘ can be advantageous for safety model checking. In particular, we highlight two main benefits: (i) this formulation enables an incremental approach with respect to the specification, wherein the model checking of 1 ∘ · · · ∘ +1 is invoked only if the verification of 1 ∘ · · · ∘ finds a counterexample, i.e., if ℒ( ) ∩ ℒ(1 ∘ · · · ∘ ) ̸= ∅; moreover, (ii) the set of reachable states computed at the i-th step can be leveraged as assumptions in the model checking of the (i+1)-th step, thereby potentially reducing the overall verification efort.
An incremental procedure for model checking cascades of automata. Let = (Σ, , , ) be a transition system and let = 1 ∘ · · · ∘ be an automata cascade over the alphabet Σ′ := × Σ used for specifying the language ℒ of bad behaviors (cf., Definition 3).
The classical approach to safety model checking [
(Σ′, 0, ) 0 (Σ′ ∖ {, }, 0) 1 0 (, 1, ) (Σ′, , ) 1
However, when the automaton specifying the property has a large number of states, this check may become impractical. This issue persists even in the case of cascades, since the state space of the cascade product is at least of size 2. Nevertheless, in the context of automata cascades, we can exploit the following proposition.
Proposition 1. If ℒ( ) ∩ ℒ(1 ∘ · · · ∘
) = ∅, for some ∈ {1, . . . , }, then ℒ( ) ∩ ℒ() = ∅.
The above proposition asserts that if there exists an index such that the model checking of with respect to 1 ∘ · · · ∘ fails to detect a violation, then no violation exists in with respect to the full specification 1 ∘ · · · ∘ . This incremental approach with respect to the specification may allow the verification process to be terminated early, before analyzing the entire cascade (in Section 5, we present case studies in which this indeed occurs).
This suggests the following incremental approach for model checking with respect to 1 ∘ · · ·∘ : 1. Initialize = 1. 2. Check whether ℒ( ) ∩ ℒ(1 ∘ · · · ∘
) = ∅. • If so, terminate: there is no bad behavior with respect to ℒ(1 ∘ · · · ∘ ).
• Otherwise, increment and repeat Step 2.
Although this approach is also possible in the case where the specification is expressed through a classical direct product of automata, a property written in the form 1 × · · · × can only capture a set of constraints combined conjunctively. This typically results in either a trivial specification or an overly complex individual automaton . In contrast, by employing a cascade product, one can express intricate properties (not merely a conjunction of separate constraints) while keeping the individual components remarkably simple–as simple as two-state automata (see Section 2).
As an example, consider the cascade 1 ∘ 2 ∘ 3 depicted in Fig. 2 for the language * Σ′* Σ′* (for sake of simplicity, here we call , , , . . . the elements of Σ′). It is worth noting that such a property cannot be defined using the classical direct product 1 × 2 × 3, except in the trivial case where one of the automata encodes the entire property while the others recognize the universal language. The incremental approach we propose intuitively performs the following checks. It first verifies whether there exists a path in that contains at least one occurrence of (this amounts to checking whether ℒ( ) ∩ ℒ(1) = ∅). If this is not the case, the procedure terminates; otherwise, it proceeds to check whether there exists a computation of that features a preceded exclusively by symbols , i.e., it checks whether ℒ( ) ∩ ℒ(1 ∘ 2) = ∅. If this not the case, the procedure terminates; otherwise, it finally verifies whether there exist violations with respect to the entire specification by checking ℒ( ) ∩ ℒ(1 ∘ 2 ∘ 3) = ∅.
Reusing the set of reachable states. Each of the steps described above efectively amounts to a reachability check: we construct the (direct) product × (1 ∘ · · · ∘ ), and verify whether at least one final state is reachable from an initial state. If this is the case, then ℒ( ) ∩ ℒ(1 ∘ · · · ∘ ) ̸= ∅, and vice versa. Typically, the reachability check between nodes and ′ is performed by computing an over-approximation of the states reachable from , and iteratively refining this set until either ′ is excluded or a path from to ′ is discovered.
Now, suppose that the -th step detects a violation, i.e., ℒ( ) ∩ ℒ(1 ∘ · · · ∘ ) ̸= ∅. During this check, we can store an over-approximation of the states reachable (from the initial state) that we have computed, and use it as a hypothesis to accelerate the (i+1)-th step. Indeed, as established by the following proposition, if a state is unreachable in × (1 ∘ · · ·∘ ), then it remains unreachable in × (1 ∘ · · ·∘ +1). Let := { ∈ 1 ∘· | = (0, 1, . . . , ), (0, . . . , ) is reachable in 1 ∘ · · · ∘ }. Proposition 2. For all ∈ {1, . . . , }, it holds that +1 ⊆ .
Thus, if is an over-approximation of the states reachable at step , the reachability check at step i+1 does not need to examine states outside of . In general, this has the potential to significantly reduce the search space, thereby yielding a substantial speed-up in the overall verification process.
In this section, we demonstrate how cascades of automata can be conveniently represented in a symbolic
manner, thereby enabling the application of eficient symbolic algorithms for safety model checking,
such as IC3 [
First, we use a separate SMV module for each component of the cascade. In fact, the notion of a cascade naturally corresponds to the concept of a “hierarchy of modules” in SMV2: the first module (corresponding to the first component of the cascade) takes as input parameters only the symbols in Σ′, whereas the second module takes as input not only Σ′ but also the state variables of the first module (in this case, ), and so on and so forth.
Second, we model the states (initial and final) and the transition function of each component by
means of Boolean state variables and formulas. Here, two considerations arise from the fact that, by
Krohn-Rhodes theorem [
VAR
x : boolean;
init(x) := FALSE; next(x) := case a : TRUE; -- if ’a’ is a reset on state x=1
. . .
VAR
x : boolean;
init(x) := FALSE; next(x) := case a : FALSE; -- if ’a’ is a reset on state x=0
. . .
Third, we specify (the complement of) the set of final states via the INVARSPEC keyword followed by the negation of the Boolean formula encoding the final states of the component under consideration. In this way, when performing model checking of with respect to, say, the first component 1, if the invariant in INVARSPEC is violated, it means that at least one final state is reachable and, according to the incremental approach described in the previous section, verification can proceed to the next component. Otherwise, verification terminates, since no final state is reachable in the first component. 2See, for instance, the statement “A module can contain instances of other modules, allowing a structural hierarchy to be built.” in the manual of the nuXmv model checker [12, Section 2.3.11]) 1 MODULE A_1(Σ′) 2 VAR 3 q : boolean; 4 ASSIGN 5 init(q) := FALSE; 6 next(q) := case 7 b : TRUE; -- resets 8 TRUE : q; -- identities 9 esac; 10 INVARSPEC 11 !q; 1 MODULE A_2(Σ′,autom1) 1 MODULE A_3(Σ′,autom1,autom2) 2 VAR 2 VAR 3 t : boolean; 3 v : boolean; 4 ASSIGN 4 ASSIGN 5 init(t) := FALSE; 5 init(v) := FALSE; 6 next(t) := case 6 next(v) := case 7 !(a|b) & !autom1.q : TRUE; 7 c & autom1.q : TRUE; 8 TRUE : t; 8 TRUE : v;
Listing 1: SMV module for 1 Listing 2: SMV module for 2 Listing 3: SMV module for 3
This section provides a proof-of-concept that illustrates the potential of the symbolic approach based on cascades of automata for safety model checking. Specifically, by considering the cascade depicted in Fig. 3 (which corresponds to the LTL formula U ( ∧ XF)) and employing the nuXmv model checker [17], we show how the incremental approach outlined in Section 3, using IC3 at each step, proves to be significantly more advantageous than verifying the entire cascade at once. Moreover, it emerged that in certain cases, our proposed approach is orders of magnitude more efective than verifying directly the equivalent LTL formula–in this case, U ( ∧ XF). 5.1. Discussion of the experimental evaluation We tested the incremental approach, implemented through the symbolic method, for model checking the property specified by the cascade 1 ∘ 2 ∘ 3 (Fig. 2), which is represented symbolically in Fig. 3. We evaluated this property on three models, shown in Fig. 4.
In the first model ( 1), there is no computation that contains at least one occurrence of . Thus, there exists no model in 1 of the property specified by the cascade. When performing model checking of 1 against the entire specification ( i.e., the full cascade 1 ∘ 2 ∘ 3), the time required by IC3 (as implemented in nuXmv) was 8.64 seconds. However, we observe that the absence of counterexamples is already captured by the first component of the cascade, namely 1, which never reaches its final state. Therefore, we also performed model checking of 1 against 1 alone, as would be done by the incremental approach described in Section 3, and found that the verification time was only 0.14 seconds. Since, as noted, there are no counterexamples even for 1, the incremental approach allows us to avoid proceeding to the verification of both 1 ∘ 2 and 1 ∘ 2 ∘ 3.
111117896543202134 TIVRNA(((Aa(dcba(IRnn(((NTee&::::dddSmxxo0bbb>><!ttd.ooob((558.oooac21)lll)&55730eee5561<<d0aaa)=--&&&0nnn=>>;;;0;0!b!;)(db)b)=d))-5&--<>5>>47!)nn8!nee&9exx|xtt((t(bb(d))b))))&&& 11116785943211023 MTIVORNA(DAdac(((baIRnnnU(NTeee:&:::dLSxxxE0bbb!!tttm.ooob(((=.oooocad91d&l)))ll90eeee<<d=80aaal=--0)nnn(>>;;;0;-(;>d(d=+d91!n<9)e97mx)8ot(9db)1))0)01&&&)); 11116785943211203 MTIVORNA(DAdac(((baIRnnnU(NTeee:&:::dLSxxxE0bbb!!tttm.ooo(((b=.oooocad95d)))&lll90eeee<<=d80aaal=--0)nnn(>>;;;0;-(;>d(d=+d41!n<9)e99mx99ot)(8db)5))0)00&&&)); 15 (next(d) = ((d+1) mod 987));
Listing 5: SMV module for 2
Listing 6: SMV module for 3 Listing 4: SMV module for 1
In model 2, every path eventually contains an occurrence of , but also has an intermediate point where does not hold, rendering 2 free of counterexamples (i.e., models of the cascade). In this case as well, verification of the entire cascade requires 24.21 seconds. Applying the incremental approach, we start by verifying automaton 1: the model checking of 1 against 2 finds a counterexample in 6.13 seconds. According to the incremental approach, we must then proceed to verify the second automaton. We simulated the reuse of the reachable states of 1 discovered in the first step by adding to 1 an invariant of the form . < 998 → ¬. With this additional information, the verification of 2 against 1 ∘ 2 takes only 0.08 seconds, and since no counterexamples are found, we can terminate without verifying 1 ∘ 2 ∘ 3.
Model 3, on the other hand, contains at least one trace in ℒ(1 ∘ 2 ∘ 3). The verification time for the entire cascade is 530.22 seconds. By contrast, using the incremental approach: (i) model checking of 1 alone takes 11.69 seconds; (ii) verification of 1 ∘ 2 ∘ 3, simulating the reuse of the reachable states of 1 by adding the invariant . < 998 → ¬, requires only 1.28 seconds. For this case, we also verified the property expressed directly by the LTL formula U ( ∧ XF), which required 408.44 seconds.
At https://users.dimi.uniud.it/~luca.geatti/data/overlay-25/SMV.zip, we provide the SMV source code for all experiments, along with detailed instructions for executing them.
This proof-of-concept highlights the potential of the symbolic approach based on cascades of automata for safety model checking. It demonstrates not only the advantages of the incremental approach–which reuses the reachable states at each iteration compared to verifying the entire cascade at once–but also its superiority over directly verifying the property expressed in LTL.
In this paper, we have shown how using cascades of automata to specify the undesired properties of a system can be beneficial in the context of safety model checking. We proposed an incremental approach that verifies components in an incremental fashion–potentially reusing information obtained from previous steps–and demonstrated how a symbolic approach to verifying cascades is also feasible.
Undoubtedly, specifying properties directly through cascades may not always be convenient, especially when compared to more declarative formalisms such as LTL. For this reason, it is crucial to develop efective methods for translating temporal logic formulas into (symbolic) cascades of automata. Moreover, an extended experimental evaluation, building on the proof-of-concept presented in Section 5, is essential to thoroughly assess the efectiveness of this approach.
Last but not least, an interesting direction for future work is to extend the cascade product to nondeterministic automata. This could simplify the specification of a property, but it would clearly make the notion of reset automata, and thus the related considerations on the structure of formulas within the corresponding SMV modules, no longer meaningful.
Luca Geatti acknowledges the support from the project “ENTAIL - intEgrazioNe tra runTime verification e mAchlne Learning” - funded by the European Union – NextGenerationEU, under the PNRR- M4C2I1.5, Program “iNEST - interconnected nord-est innovation ecosystem” - Creazione e raforzamento di “Ecosistemi dell’Innovazione per la sostenibilità” – ECS_00000043, CUP G23C22001130006 - R.S. Geatti.
During the preparation of this work, the author used ChatGPT in order to: Text Translation and Improved writing style. After using this tool/service, the author reviewed and edited the content as needed and takes full responsibility for the publication’s content. [13] E. M. Clarke, E. A. Emerson, A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst. 8 (1986) 244–263. URL: https://doi.org/10.1145/5397.5399. doi: 10.1145/5397.5399. [14] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem, Handbook of model checking, volume 10,
Springer, 2018. doi: 10.1007/978-3-319-10575-8. [15] E. M. Clarke, E. A. Emerson, J. Sifakis, Model checking: algorithmic verification and debugging,
Communications of the ACM 52 (2009) 74–84. [16] S. Bansal, Y. Li, L. M. Tabajara, M. Y. Vardi, A. M. Wells, Model checking strategies from synthesis over finite traces, in: É. André, J. Sun (Eds.), Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Singapore, October 24-27, 2023, Proceedings, Part I, volume 14215 of Lecture Notes in Computer Science, Springer, 2023, pp. 227–247. URL: https: //doi.org/10.1007/978-3-031-45329-8_11. doi: 10.1007/978-3-031-45329-8_11. [17] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, S. Tonetta, The nuXmv Symbolic Model Checker, in: CAV, 2014, pp. 334–342.