Computer Science – Logic in Computer Science
Scientific paper
2010-06-08
EPTCS 25, 2010, pp. 89-102
Computer Science
Logic in Computer Science
Scientific paper
10.4204/EPTCS.25.11
The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specification first translate the given LTL formula to an equivalent omega-automaton and then compute a winning strategy for the corresponding omega-regular game. To this end, the obtained omega-automata have to be (pseudo)-determinized where typically a variant of Safra's determinization procedure is used. In this paper, we show that this determinization step can be significantly improved for tool implementations by replacing Safra's determinization by simpler determinization procedures. In particular, we exploit (1) the temporal logic hierarchy that corresponds to the well-known automata hierarchy consisting of safety, liveness, Buechi, and co-Buechi automata as well as their boolean closures, (2) the non-confluence property of omega-automata that result from certain translations of LTL formulas, and (3) symbolic implementations of determinization procedures for the Rabin-Scott and the Miyano-Hayashi breakpoint construction. In particular, we present convincing experimental results that demonstrate the practical applicability of our new synthesis procedure.
Morgenstern Andreas
Schneider Klaus
No associations
LandOfFree
Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-29317