Thesis

Two variable and linear temporal logic in model checking and games

Abstract:

Model checking linear-time properties expressed in first-order logic has non-elementary complexity, and thus various restricted logical languages are employed. In the first part of this dissertation we consider two such restricted specification logics on words: linear temporal logic (LTL) and two-variable first-order logic (FO2). LTL is more expressive but FO2 can be more succinct, and hence it is not clear which should be easier to verify. We take a comprehensive look at the issue, giving...

Authors

More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Oxford college:
Oriel College
Role:
Author

Contributors

Role:
Supervisor
Publication date:
2013
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
Language:
English
Subjects:
UUID:
uuid:b4de8937-4a4a-4281-92e7-aa4e93283250
Local pid:
ora:8716
Deposit date:
2014-07-04