Abstract
We develop a HORNSAT-based methodology for verification of finite state systems. This general methodology leads naturally to algorithms, that are local [25, 19], on the fly [28, 11, 13, 5] and incremental [24]. It also leads naturally to diagnostic behavioral relation checking
This research was supported by NSF Grants CCR-90-06396 and CCR-94-06611.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
H. R. Andersen. Model checking and boolean graphs. Theoretical Computer Science, 126(1):3–30, 1994.
G. Ausiello, A. D'Atri, and D. Sacca. Graph algorithms for functional dependency manipulation. Journal of Association for Computing Machinery, 30(4):752–766, Oct 1983.
G. Ausiello and G. F. Italiano. On-line algorithms for polynomially solvable satisfiability problems. Journal of Logic Programming, 10:69–90, 1991.
C. Beeri. On the membership problem for functional and multivalued dependencies in relational databases. ACM Transactions on Database Systems, 5:241–259, 1980.
G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for ctl. In Proceedings of IEEE Symposium on Logic In Computer Science' 95, 1995.
J. C. Bradfield. Verifying Temporal Properties of Systems. Birkhauser, 1992.
U. Celikkan and R. Cleaveland. Generating diagnostic information for behavioral preorders. In Proceedings of Computer Aided Verification: 1992, Lecture Notes in Computer Science 663, pages 370–383, 1992.
R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27:725–747, 1990.
R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for modal mucalculus. In Proceedings of Computer Aided Verification: 1992, Lecture Notes in Computer Science 663, pages 410–422, 1992.
R. Cleaveland and B. Steffen. Computing behavioural relations, logically. In ICALP, pages 127–138, 1991.
C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
W.F. Dowling and J.H. Gallier. Linear time algorithm for testing the satisfiability of propositional horn formulae. Journal of Logic Programming, 3:267–284, 1984.
J. C. Fernandez and L. Mounier. On the fly verification of behavioral equivalences and preorders. In The 3rd International Workshop on Computer Aided Verification 1991, Lecture Notes in Computer Science 575, pages 181–191, 1991.
J. F. Groote. Private communications. 1996.
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27, 1983.
O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching time model checking. Draft, 1995.
K. G. Larsen. Proof systems for hennessy milner logic with recursion. In CAAP'88 Lecture Notes in Computer Science 299, 1988.
K. G. Larsen. Proof systems for satisfiability in hennessy-milner logic with recursion. Theoretical Computer Science, 72:265–288, 1990.
K. G. Larsen. Efficient local correctness checking. In CAV 92, Lecture Notes in Computer Science 663, pages 30–43, 1992.
X. Liu. Specification and decomposition in concurrency. Technical report, Department of Mathematics and Computer Science, Aalborg University, Denmark, 1992.
Thomas J. Schaefer. The complexity of satisfiability problems. In Tenth Annual Symposium on Theory of Computing, 1978.
S. K. Shukla, H. B. Hunt III, and D. J. Rosenkrantz. Hornsat, model checking, verification, and games. Research Report TR-95-8, Department of Computer Science, SUNY Albany, 1995.
S. K. Shukla, D. J. Rosenkrantz, H. B. Hunt III, and R. E. Stearns. A hornsat based approach to the polynomial time decidability of simulation relations for finite state processes. DIMACS workshop on Satisfiability Problem: Theory and Practice, 1996.
O. Sokolsky and S. A. Smolka. Incremental model checking in the modal mucakulus. In Proceedings of CAV'94, 1994.
C. Stirling and D. Walker. Local model checking in the modal mil-calculus. Theoretical Computer Science, 89:161–177, 1991.
Colin Stirling. Modal and temporal logics for processes. In Notes for Summer School in Logic Methods in Concurrency, pages Department of Computer Science, Aarhus University, 1993.
R.J. van Glabbeek. The linear time — branching time spectrum. Technical Report CS-R9029, Computer Science Department, CWI, Centre for Mathematics and Computer Science, Netherlands, 1990.
M. Vardi and P. Wolper. An automata theoretic approach to automatic program verification. In Proceedings of LICS 1986, pages 332–344, 1986.
S. Zhang, O. Sokolsky, and S. A. Smolka. On the parallel complexity of model checking in the modal mu-calculus. In Proceedings of LICS 1994, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Shukla, S.K., Hunt, H.B., Rosenkrantz, D.J. (1996). HORNSAT, model checking, verification and games. In: Alur, R., Henzinger, T.A. (eds) Computer Aided Verification. CAV 1996. Lecture Notes in Computer Science, vol 1102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61474-5_61
Download citation
DOI: https://doi.org/10.1007/3-540-61474-5_61
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61474-6
Online ISBN: 978-3-540-68599-9
eBook Packages: Springer Book Archive