Paper Info
Title
Derivation of the Input Conditional Formula from a Reactive System Specifictaion in Temporal Logic
Abstract
We present an algorithm which derives the input conditional formula from a reactive system specification. The input conditional formula explicitly expresses the constraints on the environment behavior which are implicitly involved in an unrealizable specification. The input conditional formula provides useful information in the specification/synthesis process for reactive systems. We use propositional linear-time temporal logic as a specification language, and our derivation algorithm is based on the tableau method for temporal logic.
Year
DOI
Venue
1994
10.1007/3-540-58468-4_184
FTRTFT
Keywords
Field
DocType
reactive system specifictaion,temporal logic,input conditional formula,reactive system,specification language
Computation tree logic,Specification language,Sequential logic,Programming language,Temporal logic of actions,Interval temporal logic,Computer science,Multimodal logic,Theoretical computer science,Linear temporal logic,Temporal logic
Conference
ISBN
Citations 
PageRank 
3-540-58468-4
9
0.70
References 
Authors
3
2
Name
Order
Citations
PageRank
Ryosei Mori190.70
Naoki Yonezaki210720.02