New predictability verification tests for discrete-event systems modeled by finite state automata

This paper deals with the problem of copredictability verification of discrete event systems (DES) modeled by automata in less restrictive scenarios, i.e., avoiding the assumptions on language liveness and absence of cycles of states connected by unobservable events only. We present necessary and sufficient conditions for a regular language to be copredictable, and adapt previous results on diagnosability verification to develop two new strategies to verify copredictability: the first one is based on a diagnoser-like automaton, and the second one by using verifiers. Copyright (C) 2020 The Authors.