Thesis icon

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...

Expand abstract

Actions


Authors


More by this author
Institution:
University of Oxford
Oxford college:
Oriel College
Department:
Mathematical, Physical & Life Sciences Division - Department of Computer Science
Role:
Author

Contributors

Role:
Supervisor
Publication date:
2013
Type of award:
DPhil
Level of award:
Doctoral
Awarding institution:
Oxford University, UK
URN:
uuid:b4de8937-4a4a-4281-92e7-aa4e93283250
Local pid:
ora:8716

Terms of use


Metrics


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP