Change search
ReferencesLink to record
Permanent link

Direct link
mu-calculus with explicit points and approximations
KTH, Superseded Departments, Microelectronics and Information Technology, IMIT.ORCID iD: 0000-0001-5432-6442
2002 (English)In: Journal of logic and computation (Print), ISSN 0955-792X, E-ISSN 1465-363X, Vol. 12, no 2, 255-269 p.Article in journal (Refereed) Published
Abstract [en]

We present a Gentzen-style sequent calculus for program verification which accommodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture, and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.

Place, publisher, year, edition, pages
2002. Vol. 12, no 2, 255-269 p.
Keyword [en]
mu-calculus, sequent calculus, program verification, compositionality, model checking, verification, systems
URN: urn:nbn:se:kth:diva-21521ISI: 000175399900004OAI: diva2:340219
QC 20100525Available from: 2010-08-10 Created: 2010-08-10Bibliographically approved

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Dam, MadsGurov, Dilian
By organisation
Microelectronics and Information Technology, IMIT
In the same journal
Journal of logic and computation (Print)

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 20 hits
ReferencesLink to record
Permanent link

Direct link