Symmetric temporal theorem proving

Niknafs-Kermani, A, Konev, B ORCID: 0000-0002-6507-0494 and Fisher, M (2012) Symmetric temporal theorem proving Master of Philosophy thesis, University of Liverpool.

Text 200575472_May2017.pdf - Unspecified Download (401kB)

Abstract

In this paper we consider the deductive verification of propositional temporal logic specifications of symmetric systems. In particular, we provide a heuristic approach to the scalability problems associated with analysing properties of large numbers of processes. Essentially, we use a temporal resolution procedure to verify properties of a system with few processes and then generalise the outcome in order to reduce the verification complexity of the same system with much larger numbers of processes. This provides a practical route to deductive verification for many systems comprising identical processes. © 2012 IEEE.

Item Type:	Thesis (Master of Philosophy)
Uncontrolled Keywords:	4613 Theory Of Computation, 46 Information and Computing Sciences
Divisions:	Faculty of Science & Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	21 Aug 2017 08:41
Last Modified:	22 May 2026 21:00
DOI:	10.1109/TIME.2012.20
Related Websites:	Publisher
Supervisors:	Boris Konev Michael Fisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3007705
Disclaimer:	The University of Liverpool is not responsible for content contained on other websites from links within repository metadata. Please contact us if you notice anything that appears incorrect or inappropriate.