Symmetric Temporal Theorem Proving



Niknafs-Kermani, Amir, Konev, Boris ORCID: 0000-0002-6507-0494 and Fisher, Michael
(2012) Symmetric Temporal Theorem Proving. Master of Philosophy thesis, University of Liverpool.

[img] 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)
Divisions: Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User: Symplectic Admin
Date Deposited: 21 Aug 2017 08:41
Last Modified: 19 Jan 2023 07:03
DOI: 10.17638/03007705
Related URLs:
Supervisors:
  • Boris Konev,
  • Michael Fisher,
URI: https://livrepository.liverpool.ac.uk/id/eprint/3007705