Journal article icon

Journal article

A saturation method for the modal mu-calculus over pushdown systems

Abstract:

We present an algorithm for computing directly the denotation of a μ-calculus formula χ over the configuration graph of a pushdown system. Our method gives the first extension of the saturation technique to the full μ-calculus. Finite word automata are used to represent sets of pushdown configurations. Starting from an initial automaton, we perform a series of automaton manipulations which compute the denotation by recursion over the structure of the formula. We introduce notions of under-app...

Expand abstract
Publication status:
Published

Actions


Access Document


Publisher copy:
10.1016/j.ic.2010.12.004
Journal:
INFORMATION AND COMPUTATION More from this journal
Volume:
209
Issue:
5
Pages:
799-821
Publication date:
2011-05-01
DOI:
EISSN:
1090-2651
ISSN:
0890-5401
Language:
English
Keywords:
Pubs id:
pubs:328275
UUID:
uuid:697dcf86-5e03-441c-926d-a7bc8e9e7395
Local pid:
pubs:328275
Source identifiers:
328275
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