Dependency Tree Automata (2009)
Abstract. We introduce a new kind of tree automaton, a dependency tree automaton, that is suitable for deciding properties of classes of terms with binding. Two kinds of such automaton are defined,...
DECIDABILITY OF HIGHER-ORDER MATCHING (2009)
Abstract. We show that the higher-order matching problem is decidable using a gametheoretic argument.
Decidability of higher-order matching (2009)
We show that the higher-order matching problem is decidable using a game-theoretic argument.
Tim Kempster, Colin Stirling, Peter Thanisch
Several DBMS vendors have implemented the ANSI standard SQL isolation levels for transaction processing. This has created a gap between database practice and textbook accounts of transaction...
GDP Festschrift ENTCS, to appear (2008)
Abstract We consider the transfer of verification techniques to structures with binding.
Local Model Checking Games (2008)
Extended Abstract, Colin Stirling
1 Introduction Model checking is a very successful technique for verifying temporal properties of finite state concurrent systems. It is standard to view this method as essentially algorithmic, and...
A Formal Analysis of 2PC and related Optimisations (2007)
Tim Kempster, Colin Stirling, Peter Thanisch
The Centralised Two Phase Commit Protocol (2PC) is the most widely used protocol in commercial distributed systems. Many variants of this protocol exist which try to reduce both the number of...
Games--Based Model Checking of Protocols: counting doesn't count (2007)
Tim Kempster Colin, Colin Stirling, Peter Thanisch
We introduce a technique that can be used to model the behaviour of protocols. In our model each process within a protocol belongs to a particular class. A set of rules governs the behaviour of a...
Introduction Two schema problems from the 1970s are examined, monadic recursion schemes and first-order recursion schemas. Research on these problems halted because they were shown to be equivalent...
Many Interesting Concurrent, Julian Bradfield, Colin Stirling
this paper is: can model checking techniques, as introduced in [Clarke et al.], be extended from finite to infinite state spaces? (Pragmatically, this means moving from automated to computer-aided...
Solving Parity Games in Polynomial Time (2007)
We show that there is a polynomial time algorithm for solving parity games with the consequence that the complexity of model checking modal -calculus is, therefore, also in polynomial time.
Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes (2007)
In the past decade there has been a variety of results showing decidability of bisimulation equivalence between infinite state systems. The initial result, due to Baeten, Bergstra and Klop [1],...
Bisimulation and Language Equivalence (2007)
One way to understand an interactive system is firmly rooted in language theory, that a system is its set of runs (or words). Properties of systems are described in a linear time temporal logic....
Baeten, Bergstra, and Klop (and later Caucal) have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much...
Satisfiability and Completeness of PDL replayed (2007)
Abstract. This paper reinvestigates satisfiability and completeness for PDL. Automata-theoretic methods have been successful for solving satisfiability so far, but it is not known how to use them for...
Satisfiability Games for CTL* (2007)
This paper defines games for the full branching time logic CTL # . They provide a direct method to check satisfiability of a formula since they work on its subformulas only. Thus, this method avoids...
Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes (2007)
this paper we examine the decision problem of weak bisimilarity for normed BP processes. Esparza [6] observes that weak bisimilarity is semidecidable, because a positive witness is semilinear....
the Principles of Programming Lnguages (POPL 99), 1999. (2007)
Order Mads Tofte, M. Tofte, L. Birkedal, M. Elsman, Mads Tofte, Gordon Plotkin, ...
Publications and notes in chronological
Automatic Synthesis of Dis trib (2006)
Elektrotechnik Und Informationstechnik, Aus Slatina Rumänien, Vorsitzender Prüfungsausschusses, Prof Dr, Volker Diekert, ...
ut Alin S¸tefănescu
Deciding DPDA equivalence is primitive recursive (2002)
Despite intensive work throughout the late 1960s and 1970s, the equivalence problem for determinisitic pushown automata, DPDA, whether language equivalence is decidable for deterministic context-free...
Deciding DPDA equivalence is primitive recursive (2002)
A determinisitic decision procedure for deciding equivalence of determinisitic context-free languages is presented. An upper bound on the complexity of the procedure is given that is primitive...
Model checking fixed point logic with chop (2002)
Abstract. This paper examines FLC, which is the modal µ-calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is...
Deciding DPDA equivalence is primitive recursive (2002)
Abstract. Recently Senizergues showed decidability of the equivalence problem for deterministic pushown automata. The proof of decidability is two semi-decision procedures that do not give a...
Model checking fixed point logic with chop (2002)
Modal and temporal logics are well established research areas in computer science, artificial intelligence, philosophy, etc. [2, 4, 10]. An important temporal logic is Kozen's modal-calculus L...
Deciding DPDA equivalence is primitive recursive (2002)
A determinisitic decision procedure for deciding equivalence of determinisitic context-free languages is presented. An upper bound on the complexity of the procedure is given that is primitive...
Model checking games for branching time logics (2002)
This paper defines and examines model checking games for the branching time temporal logic CTL #. The games employ a technique called focus which enriches sets by picking out one distinguished...
Model Checking Fixed Point Logic with Chop (2002)
Martin Lange And, Martin Lange, Colin Stirling
This paper examines FLC, which is the modal -calculus enriched with a sequential composition operator. Bisimulation invariance and the tree model property are proved. Its succinctness is compared to...
Deciding DPDA equivalence is primitive recursive (2002)
Abstract. Recently Sénizergues showed decidability of the equivalence problem for deterministic pushown automata. The proof of decidability is two semi-decision procedures that do not give a...
Model Checking Games for Branching Time Logics (2002)
Lange, Martin, Stirling, Colin
This paper defines and examines model checking games for the branching time temporal logic CTL*. The games employ a technique called focus which enriches sets by picking out one distinguished...
Focus games for satisfiability and completeness of temporal logic (2001)
We introduce a simple game theoretic approach to satisfiability checking of temporal logic, for LTL and CTL, which has the same complexity as using automata. The mechanisms involved are both explicit...
Bisimulation and Language Equivalence (2001)
this paper we make some contrasts between bisimulation equivalence and language equivalence. There are two threads. First is that because bisimulation is more intensional, results in language and...
Focus Games for Satisfiability and Completeness of Temporal Logic (2001)
Martin Lange Colin, Colin Stirling
We introduce a simple game theoretic approach to satisfiability checking of temporal logic, for LTL and CTL, which has the same complexity as using automata. The mechanisms involved are both explicit...
Focus games for satisfiability and completeness of temporal logic (2001)
We introduce a simple game theoretic approach to satisfiability checking of temporal logic, for LTL and CTL, which has the same complexity as using automata. The mechanisms involved are both explicit...
Modal Logics and Mu-Calculi: An Introduction (2001)
Julian Bradfield, Julian Brad Eld, Colin Stirling
We briey survey the background and history of modal and temporal logics. We then concentrate on the modal mu-calculus, a modal logic which subsumes most other commonly used logics. We provide an...
Focus games for satisfiability and completeness of temporal logic (2001)
We introduce a simple game theoretic approach to satisfiability checking of temporal logic, for LTL and CTL, which has the same complexity as using automata. The mechanisms involved are both explicit...
Model checking games for CTL (2000)
We define model checking games for the temporal logic CTL # and prove their correctness. They provide a technique for using model checking interactively in a verification /specification process....
Decidability of Bisimulation Equivalence for Pushdown Processes (2000)
We show that bisimulation equivalence is decidable for pushdown automata without #-transitions. 1 Introduction Automata and language theory studies finitely presented mechanisms for generating...
Decidability of Bisimulation Equivalence for Pushdown Processes (2000)
Colin Stirling, Colin Stirling, Colin Stirling
We show that bisimulation equivalence is decidable for pushdown automata without epsilon-transitions.
Tim Kempster, Colin Stirling, Peter Thanisch
Several DBMS vendors have implemented the ANSI standard SQL isolation levels for transaction processing. This has created a gap between database practice and textbook accounts which simply equate...
Tim Kempster, Colin Stirling, Peter Thanisch
Several DBMS vendors have implemented the ANSI standard SQL isolation levels for transaction processing. This has created a gap between database practice and textbook accounts of transaction...
A Critical Analysis of the Transaction Internet Protocol (1999)
Tim Kempster, Colin Stirling, Peter Thanisch
Recently, the Transaction Internet Protocol (TIP) became an Internet standard. TIP is intended to facilitate electronic commerce transactions in which the customer may need to acquire a package of...
Decidability of DPDA equivalence (1999)
A proof of decidability of equivalence between deterministic pushdown automata is presented using a mixture of methods developed in concurrency and language theory. The technique appeals to a tableau...
Lower Isolation Levels in Distributed Transactions (1999)
Tim Kempster, Colin Stirling, Peter Thanisch
We extend the notion of conflicting actions within transaction schedules and derive a definition of conflict serializability. Phenomenon based definitions of isolation have been presented in[1][2]....
A critical analysis of the transaction internet protocol (1999)
Tim Kempster, Colin Stirling, Peter Thanisch
Recently, the Transaction Internet Protocol (TIP) became an Internet standard. TIP is intended to facilitate electronic commerce transactions in which the customer may need to acquire a package of...
The Joys of Bisimulation (1998)
this paper we review results about bisimulation, from both the point of view of automata and from a logical point of view. We also consider how bisimulation has a role in finite model theory, and we...
Practical Model-Checking Using Games (1998)
Perdita Stevens, Colin Stirling
. We describe how model-checking games can be the foundation for efficient local model-checking of the modal mu-calculus on transition systems. Game-based algorithms generate winning strategies for a...
Practical Model-Checking Using Games (1998)
Perdita Stevens, Colin Stirling
. We describe how model-checking games can be the foundation for efficient local model-checking of the modal mu-calculus on transition systems. Game-based algorithms generate winning strategies for a...
A More Committed Quorum-Based Three Phase Commit Protocol (1998)
Tim Kempster Colin, Colin Stirling, Peter Thanisch
Introduction As computing equipment is getting increasingly reliable, distributed transaction processing environments e.g. mobile computing, Internet commerce and replication, are becoming...
Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes (1998)
Baeten, Bergstra, and Klop (and later Caucal) have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much...
Decidability of Bisimulation Equivalence for Normed Pushdown Processes (1996)
We prove that bisimulation equivalence is decidable for normed pushdown processes. 1 Introduction In the classical theory of automata the expressive power of pushdown automata is matched by...
Decidability of Bisimulation Equivalence for Normed Pushdown Processes (1996)
this paper we prove that bisimulation equivalence is decidable for this richer family of processes. However the proof is not easy, and does not follow immediately from the techniques used for showing...
Games and Modal Mu-Calculus (1996)
We define Ehrenfeucht-Fraiss'e games which exactly capture the expressive power of the extremal fixed point operators of modal mucalculus. The resulting games have significance, we believe,...
Modal and Temporal Logics for Processes (1996)
this paper have been presented at the 4th European Summer School in Logic, Language and Information, University of Essex, 1992; at the Tempus Summer School for Algebraic and Categorical Methods in...
Modal and Temporal Logics for Processes (1996)
Colin Stirling Dept, Colin Stirling
this paper have been presented at the 4th European Summer School in Logic, Language and Information, University of Essex, 1992; at the Tempus Summer School for Algebraic and Categorical Methods in...
Model Checking and Other Games (1996)
Contents 1 Introduction 2 2 Process Calculi 2 3 Equivalences, Modal and Temporal Logics 5 3.1 Interactive games and bisimulations . . . . . . . . . . . . . . . 7 3.2 Modal logic and bisimulations . ....
Bisimulation Equivalence is Decidable for all Context-Free Processes (1995)
Søren Christensen, Hans Hüttel, Colin Stirling
Introduction Over the past decade much attention has been devoted to the study of process calculi such as CCS, ACP and CSP [13]. Of particular interest has been the study of the behavioural semantics...
A compositional proof system for the modal -calculus (1994)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel, Colin Stirling Glynn
et al.: A
A compositional proof system for the modal -calculus (1994)
Henrik Reif Andersen, Henrik Reif Andersen, Colin Stirling, Colin Stirling, Glynn Winskel, Glynn Winskel
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
A Compositional Proof System for the Modal (1994)
Calculus Henrik Reif, Henrik Reif Andersen, Colin Stirling, Glynn Winskel
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal - calculus. The proof system is compositional in the structure...
A Compositional Proof System for the Modal µ-Calculus (1994)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel
We present a proof system for determining satisfaction between processes in a fairly general process algebra and assertions of the modal ¯- calculus. The proof system is compositional in the...
A compositional proof system for the modal µ-calculus (1994)
Henrik Reif Andersen, Colin Stirling, Glynn Winskel, Henrik Reif, Andersen Colin, Stirling Glynn Winskel
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent BRICS...
Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes (1993)
Baeten, Bergstra, and Klop (and later Caucal) have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much...
Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes (1993)
Baeten, Bergstra, and Klop (and later Caucal) have proved the remarkable result that bisimulation equivalence is decidable for irredundant context-free grammars. In this paper we provide a much...