An Exponential Lower Bound for the Latest Deterministic Strategy Iteration Algorithms [PDF]
Logical Methods in Computer Science, 2011 This paper presents a new exponential lower bound for the two most popular deterministic variants of the strategy improvement algorithms for solving parity, mean payoff, discounted payoff and simple stochastic games. The first variant improves every node
Oliver Friedmann
doaj +1 more source
Improved Algorithms for Parity and Streett objectives [PDF]
Logical Methods in Computer Science, 2017 The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness ...
Krishnendu Chatterjee +2 more
doaj +1 more source
Efficient Open World Reasoning for Planning [PDF]
Logical Methods in Computer Science, 2006 We consider the problem of reasoning and planning with incomplete knowledge and deterministic actions. We introduce a knowledge representation scheme called PSIPLAN that can effectively represent incompleteness of an agent's knowledge while allowing for ...
Tamara Babaian, James G. Schmolze
doaj +1 more source
Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic [PDF]
Logical Methods in Computer Science, 2007 In a previous work Baillot and Terui introduced Dual light affine logic (DLAL) as a variant of Light linear logic suitable for guaranteeing complexity properties on lambda calculus terms: all typable terms can be evaluated in polynomial time by beta ...
Vincent Atassi +2 more
doaj +1 more source
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning [PDF]
Logical Methods in Computer Science, 2008 Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there is no regularity condition.
Samuel R. Buss +2 more
doaj +1 more source
Representations of Stream Processors Using Nested Fixed Points [PDF]
Logical Methods in Computer Science, 2009 We define representations of continuous functions on infinite streams of discrete values, both in the case of discrete-valued functions, and in the case of stream-valued functions.
Neil Ghani +2 more
doaj +1 more source
Unique perfect matchings, forbidden transitions and proof nets for linear logic with Mix [PDF]
Logical Methods in Computer Science, 2020 This paper establishes a bridge between linear logic and mainstream graph theory, building on previous work by Retor\'e (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect ...
Lê Thành Dũng Nguyên
doaj +1 more source
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes [PDF]
Logical Methods in Computer Science, 2009 We propose a framework for reasoning about unbounded dynamic networks of infinite-state processes. We propose Constrained Petri Nets (CPN) as generic models for these networks.
Ahmed Bouajjani +4 more
doaj +1 more source
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems [PDF]
Logical Methods in Computer Science, 2012 We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity.
Takahito Aoto, Yoshihito Toyama
doaj +1 more source
Visibly Tree Automata with Memory and Constraints [PDF]
Logical Methods in Computer Science, 2008 Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison.
Hubert Comon-Lundh +2 more
doaj +1 more source