LTL Monitoring Algorithm2.3

From FSL
Jump to: navigation, search

Finite state machines are generated from the LTL specification by going through alternating automata based on the work available here. The resultant Buchi automata are converted to finite state machines suitable for monitoring using the algorithm presented in Efficient_Monitoring_of_Omega-Languages.To monitor the finite state machine the normal finite state machine monitoring algorithm is used. Because not all events of interest are necessarily used in a PTLTL formula, there is a default transition in every FSM state.

Personal tools