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.
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: |
|
URI: | https://livrepository.liverpool.ac.uk/id/eprint/3007705 |