Journal article icon

Journal article

Two Variable vs. Linear Temporal Logic in Model Checking and Games

Abstract:

Verification tasks have non-elementary complexity for properties of linear traces specified in first-order logic, and thus various limited logical languages are employed. In this paper we consider two restricted specification logics, linear temporal logic (LTL) and two-variable first-order logic (FO 2). LTL is more expressive, but FO 2 is often more succinct, and hence it is not clear which should be easier to verify. In this paper we take a co...

Expand abstract
Publication status:
Published

Actions


Access Document


Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
Journal:
CONCUR 2011: CONCURRENCY THEORY More from this journal
Volume:
6901
Pages:
497-511
Publication date:
2011-01-01
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
Language:
English
Pubs id:
pubs:305622
UUID:
uuid:ca74563a-7b39-4c2f-8788-db434a003e34
Local pid:
pubs:305622
Source identifiers:
305622
Deposit date:
2012-12-19

Terms of use


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