Generating models of infinite-state communication protocols using regular inference with abstraction
In order to facilitate model-based verification and validation, effort is underway to develop techniques for generating models of communication system components from observations of their external behavior. Most previous such work has employed regular ...
A game approach to determinize timed automata
Timed automata are frequently used to model real-time systems. Their determinization is a key issue for several validation problems. However, not all timed automata can be determinized, and determinizability itself is undecidable. In this paper, we ...
Vacuity in practice: temporal antecedent failure
Different definitions of vacuity in temporal logic model checking have been suggested along the years. Examining them closely, however, reveals an interesting phenomenon. On the one hand, some of the definitions require high-complexity vacuity detection ...