Journal article icon

Journal article

Branching-time model checking of parametric one-counter automata

Abstract:

We study the computational complexity of model checking EF logic and modal logic on parametric one-counter automata (POCA). A POCA is a one-counter automaton whose counter updates are either integer values encoded in binary or integer-valued parameters. Given a formula and a configuration of a POCA, the model-checking problem asks whether the formula is true in this configuration for all possible valuations of the parameters. We show that this problem is undecidable for EF logic via reduction...

Expand abstract

Actions


Access Document


Authors


More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Role:
Author
Journal:
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume:
7213 LNCS
Pages:
406-420
Publication date:
2012-01-01
DOI:
EISSN:
1611-3349
ISSN:
0302-9743
URN:
uuid:c52cdee6-1f32-49dd-bf62-70746febb857
Source identifiers:
323301
Local pid:
pubs:323301
Language:
English

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