Verification of Non-Regular Properties

[Harel et al., 1983]

D. Harel and A. Pnueli and J. Stavi (1983).
Propositional Dynamic Logic of Nonregular Programs.
In: Journal of Computer and System Sciences, 26(2):222--243.

[Harel and Singerman, 1996]

D. Harel and E. Singerman (1996).
More on Nonregular PDL: Finite Models and Fibonacci-Like Programs.
In: Information and Computation, 128(2):109--118.

[Müller-Olm, 1999]

M. Müller-Olm (1999).
A Modal Fixpoint Logic with Chop.
In: Christoph Meinel and Sophie Tison (eds.), Proc.\ 16th.\ Symposium on Theoretical Aspects in Computer Science, STACS'99. Volume 1563 of LNCS. Trier, Germany, pp. 510--520. Published by Springer.

[Lange and Stirling, 2002]

M. Lange and C. Stirling (2002).
Model Checking Fixed Point Logic with Chop.
In: M. Nielsen and U. H. Engberg (eds.), Proc.\ 5th Conf.\ on Foundations of Software Science and Computation Structures, FOSSACS'02. Volume 2303 of LNCS. Grenoble, France, pp. 250--263. Published by Springer.

[Lange, 2002]

M. Lange (2002).
Alternating Context-Free Languages and Linear Time $\mu$-Calculus with Sequential Composition.
In: P. Panangaden and U. Nestmann (eds.), Proc.\ 9th Workshop on Expressiveness in Concurrency, EXPRESS'02. Volume 68.2 of ENTCS. Brno, Czech Republic, pp. 71--87. Published by Elsevier.

[Lange, 2002]

M. Lange (2002).
Local Model Checking Games for Fixed Point Logic with Chop.
In: L. Brim and P. Jan\vcar and M. K\vretínský and A. Ku\vcera (eds.), Proc.\ 13th Conf.\ on Concurrency Theory, CONCUR'02. Volume 2421 of LNCS. Brno, Czech Republic, pp. 240--254. Published by Springer.

[Viswanathan and Viswanathan, 2004]

Mahesh Viswanathan and Ramesh Viswanathan (2004).
A Higher Order Modal Fixed Point Logic.
In: Philippa Gardner and Nobuko Yoshida (eds.), Proc.\ 15th Int.\ Conference on Concurrency Theory, CONCUR'04. Volume 3170 of LNCS. London, UK, pp. 512--528. Published by Springer.

[Lange and Loidl, 2004]

M. Lange and H. W. Loidl (2004).
Parallel and Symbolic Model Checking for Fixpoint Logic with Chop.
In: L. Brim and M. Leucker (eds.), Proc.\ 3rd Int.\ Workshop on Parallel and Distributed Methods in Verification, PDMC'03. Volume 1283 of ENTCS. London, UK, pp. 125--138. Published by Elsevier.

[Dawar et al., 2004]

Anuj Dawar and Erich Grädel and Stephan Kreutzer (2004).
Inflationary fixed points in modal logic.
In: ACM Transations on Computational Logic, 5(2):282--315.

[Lange and Somla, 2005]

M. Lange and R. Somla (2005).
The Complexity of Model Checking Higher Order Fixpoint Logic.
In: J. Jedrzejowicz and A. Szepietowski (eds.), Proc.\ 30th Int.\ Symp.\ on Math.\ Foundations of Computer Science, MFCS'05. Volume 3618 of LNCS. Gdansk, Poland, pp. 640--651. Published by Springer.

[Lange, 2005]

Martin Lange (2005).
Model Checking Propositional Dynamic Logic with All Extras.
In: Journal of Applied Logic, 4(1):39--49.

[Lange, 2005]

Martin Lange (2005).
Temporal Logics for Non-Regular Properties: Model Checking.
In: H. Schlingloff (ed.), Proc.\ 4th Int.\ Workshop on Methods for Modalities, M4M-4. Volume 194 of Informatik Berichte. Berlin, Germany, pp. 1--7. Published by HU Berlin.

[Zhan and Wu, 2005]

Naijun Zhan and Jinzhao Wu (2005).
Compositionality of Fixpoint Logic with Chop..
In: Dang Van Hung and Martin Wirsing (eds.), Proc.\ Second International Colloquium on Theoretical Aspects of Computing ICTAC'05. Volume 3722 of LNCS. Hanoi, Vietnam, pp. 136--150. Published by Springer.

[Lange, 2006]

Martin Lange (2006).
Temporal Logics Beyond Regularity.

[Lange, 2006]

M. Lange (2006).
The Alternation Hierarchy in Fixpoint Logic with Chop Is Strict Too.
In: Information and Computation, 204(9):1346--1367.

[Lange and Somla, 2006]

M. Lange and R. Somla (2006).
Propositional Dynamic Logic of Context-Free Programs and Fixpoint Logic with Chop.
In: Information Processing Letters, 100(2):72--75.

[Löding and Serre, 2006]

Christof Löding and Olivier Serre (2006).
Propositional Dynamic Logic with Recursive Programs.
In: Luca Aceto and Anna Ingólfsdóttir (eds.), Proc.\ 9th Int.\ Conf.\ on Foundations of Software Science and Computation Structures, FOSSACS '06. Volume 3921 of LNCS. Vienna, Austria, pp. 292--306. Published by Springer.

[Axelsson et al., 2007]

Roland Axelsson and Martin Lange and Rafal Somla (2007).
The Complexity of Model Checking Higher Order Fixpoint Logic.
In: Logical Methods in Computer Science, 3(2):1--33.

[Axelsson and Lange, 2007]

R. Axelsson and M. Lange (2007).
Model Checking the First Order Fragment of Higher-Order Fixpoint Logic.
In: N. Dershowitz and A. Voronkov (eds.), Proc.\ 14th Int.\ Conf.\ on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR'07. Volume 4790 of LNCS. Yerevan, Armenia, pp. 62--76. Published by Springer.

[Kreutzer and Lange, 2007]

S. Kreutzer and M. Lange (2007).
Non-Regular Fixpoint Logic and Games.
In: E. Grädel and J. Flum and T. Wilke (eds.), Logic and Automata: History and Perspectives. Volume 2 of Texts in Logic and Games. pp. 433--466. Amsterdam University Press.

[Lange, 2007]

M. Lange (2007).
Three Notes on the Complexity of Model Checking Fixpoint Logic with Chop.
In: R.A.I.R.O. -- Theoretical Informatics and Applications, 41:177--190.