Efficient Translation of LTL to Büchi Automata

The construction of Büchi automata from linear temporal logic is a significant step in model check-ing. This paper presents a depth-first construction algorithm to obtain simple Büchi automata from linear-time temporal logic which significantly reduces the sizes of the state spaces. A form-filling algorithm was used to reduce the size of the generated automata and the algorithms were applied directly to state-based Büchi automata, without transformation into transition-based automata. A form-filling algorit...     

Verification of Interdomain Routing System Based on Formal Methods

In networks,the stable path problem (SPP) usually results in oscillations in interdomain systems and may cause systems to become unstable.With the rapid development of internet technology,the occurrence of SPPs in interdomain systems has quite recently become a significant focus of research.A framework for checking SPPs is presented in this paper with verification of an interdomain routing system using formal methods and the NuSMV software.Sufficient conditions and necessary conditions for determining SPP occurrence are presented with proof of the method's effectiveness.Linear temporal logic was used to model an interdomain routing system and its properties were analyzed.An example is included to demonstrate the method's reliability.