# Combining Explicit and Symbolic LTL Model Checking Using Generalized Testing Automata

## Abstract

In automata-theoretic model checking, there are mainly two approaches: explicit and emphsymbolic. In the explicit approach, the state-space is constructed explicitly and lazily during exploration (i.e.on-the-fly). The symbolic approach tries to overcome the state-space explosion obstacle by symbolically encoding the state-space in a concise way using decision diagrams. However, this symbolic construction is not performed on-the-fly as in the explicit approach. In order to take advantage of the best of both worlds, emphhybrid approaches are proposed as combinations of explicit and symbolic approaches. A hybrid approach is usually based on an on-the-fly construction of an explicit graph of symbolic nodes, where each symbolic node encodes a subset of states by means of binary decision diagrams. An alternative to the standard Büchi automata, called Testing automata have never been used before for hybrid model checking. In addition, in previous work, we have shown that Generalized Testing Automata (TGTA) can outperform the Büchi automata for explicit and symbolic model checking of stutter-invariant LTL properties. In this workwe investigate the use of these TGTA to improve hybrid model checking. We show how traditional hybrid approaches based on Generalized Büchi Automata (TGBA) can be adapted to obtain TGTA-based hybrid approaches. Then, each original approach is experimentally compared against its TGTA variant. The results show that these new variants are statistically more efficient.

## Bibtex (lrde.bib)

@InProceedings{	  bensalem.15.acsd,
author	= {Ala Eddine Ben{ S}alem and Mohamed Graiet},
title		= {Combining Explicit and Symbolic {LTL} Model Checking Using
Generalized Testing Automata},
booktitle	= {Proceedings of the 15th International Conference on
Application of Concurrency to System Design (ACSD'15)},
year		= 2015,
month		= jun,
publisher	= {IEEE Computer Society},
abstract	= {In automata-theoretic model checking, there are mainly two
approaches: \emph{explicit} and \emph{symbolic}. In the
explicit approach, the state-space is constructed
explicitly and lazily during exploration (i.e.,
on-the-fly). The symbolic approach tries to overcome the
state-space explosion obstacle by symbolically encoding the
state-space in a concise way using decision diagrams.
However, this symbolic construction is not performed
on-the-fly as in the explicit approach. In order to take
advantage of the best of both worlds, \emph{hybrid
approaches} are proposed as combinations of explicit and
symbolic approaches. A hybrid approach is usually based on
an on-the-fly construction of an explicit graph of symbolic
nodes, where each symbolic node encodes a subset of states
by means of binary decision diagrams. An alternative to the
standard {B\"u}chi automata, called Testing automata have
never been used before for hybrid model checking. In
addition, in previous work, we have shown that
\emph{Generalized Testing Automata} (TGTA) can outperform
the {B\"u}chi automata for explicit and symbolic model
checking of stutter-invariant LTL properties. In this work,
we investigate the use of these TGTA to improve hybrid
model checking. We show how traditional hybrid approaches
based on Generalized {B\"u}chi Automata (TGBA) can be
adapted to obtain TGTA-based hybrid approaches. Then, each
original approach is experimentally compared against its
TGTA variant. The results show that these new variants are
statistically more efficient. }
}