Expressing interesting properties of programs in propositional temporal logic
作者： Pierre Wolper
关键词: Intermediate logic 、 Interval temporal logic 、 Well-formed formula 、 Linear temporal logic 、 Propositional variable 、 Computer science 、 Dynamic logic (modal logic) 、 Zeroth-order logic 、 Autoepistemic logic 、 Programming language
摘要: We show that the class of properties programs expressible in propositional temporal logic can be substantially extended if we assume to data-independent. Basically, a program is data-independent its behavior does not depend on specific data it operates upon. Our results significantly extend applicability verification and synthesis methods based logic.
acm.org
sci-hub.se 参考文章(35)
Amir Pnueli, Linear and Branching Structures in the Semantics and Logics of Reactive Systems international colloquium on automata, languages and programming. pp. 15- 32 ,(1985) , 10.1007/BFB0015727
David Harel, First-Order Dynamic Logic ,(1979)
Moshe Y. Vardi, Pierre Wolper, Yet another process logic Logics of Programs. ,vol. 164, pp. 501- 512 ,(1984) , 10.1007/3-540-12896-4_383
E. Clarke, B. Mishra, Automatic verification of asynchronous circuits Logics of Programs. pp. 101- 115 ,(1984) , 10.1007/3-540-12896-4_358
Robert Goldblatt, SEMANTICAL CONSIDERATIONS ON FLOYD-HOARE LOGIC Journal of Symbolic Logic. ,vol. 51, ,(1976) , 10.2307/2273958
Edmund M. Clarke, E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic Logic of Programs, Workshop. pp. 52- 71 ,(1981) , 10.1007/BFB0025774
Friedrich H. Vogt, Event-Based Temporal Logic Specifications of Services and Protocols Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 63- 73 ,(1982)
David Harel, Dexter Kozen, Rohit Parikh, Process logic: Expressiveness, decidability, completeness Journal of Computer and System Sciences. ,vol. 25, pp. 144- 170 ,(1982) , 10.1016/0022-0000(82)90003-4
Amir Pnueli, The temporal semantics of concurrent programs Theoretical Computer Science. ,vol. 13, pp. 45- 60 ,(1981) , 10.1016/0304-3975(81)90110-9
K. A. Bartlett, R. A. Scantlebury, P. T. Wilkinson, A note on reliable full-duplex transmission over half-duplex links Communications of The ACM. ,vol. 12, pp. 260- 261 ,(1969) , 10.1145/362946.362970