In this paper we present our PVS implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive LTL system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems - systems in which the number of processes is unbounded - and our verification rules are appropriate to such systems. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Pnueli, A., & Arons, T. (2004). TLPVS: A PVS-based LTL verification system. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2772, 598–625. https://doi.org/10.1007/978-3-540-39910-0_26
Mendeley helps you to discover research relevant for your work.