Two variable and linear temporal logic in model checking and games

Thesis

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

Authors: Lenhardt, R

• Publication date: 2013
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: Oxford University, UK
• Language: English
• Subjects: Computer science (mathematics); Probability theory and stochastic processes