Publications associées à PSPACE-complete

Uniform parsing for hyperedge replacement grammars

It is well known that hyperedge-replacement grammars can generate NP-complete graph languages even under seemingly harsh restrictions. This means that the parsing problem is difficult even in the non-uniform setting, in which the grammar is considered to b ...

ACADEMIC PRESS INC ELSEVIER SCIENCE2021

Fixed-structure Control of LTI Systems with Polytopic-type Uncertainty : Application to Inverter-interfaced Microgrids

Mahdieh Sadat Sad Abadi

This thesis focuses on the development of robust control solutions for linear time-invariant interconnected systems affected by polytopic-type uncertainty. The main issues involved in the control of such systems, e.g. sensor and actuator placement, control ...

EPFL2016

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux ...

Springer-Verlag Berlin2015

Induction for SMT Solvers

Viktor Kuncak, Andrew Joseph Reynolds

Satisfiability modulo theory solvers are increasingly being used to solve quantified formulas over structures such as integers and term algebras. Quantifier instantiation combined with ground decision procedure alone is insufficient to prove many formulas ...

Springer-Verlag2015

An Optimal Linear-Time Algorithm for Interprocedural Register Allocation in High Level Synthesis Using SSA Form

Paolo Ienne, Philip Brisk, Ajay Kumar Verma

An optimal linear-time algorithm for interprocedural register allocation in high level synthesis is presented. Historically, register allocation has been modeled as a graph coloring problem, which is nondeterministic polynomial time-complete in general; ho ...

2010

Enhancing numerical constraint propagation using multiple inclusion representations

Boi Faltings, Xuan-Ha Vu

Building tight and conservative enclosures of the solution set is of crucial importance in the design of efficient complete solvers for numerical constraint satisfaction problems (NCSPs). This paper proposes a novel generic algorithm enabling the cooperati ...

Springer Netherlands2009

Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unk ...

2008

Real-time reduced basis solutions for Navier-Stokes equations: optimization of parametrized bypass configurations

Gianluigi Rozza

The reduced basis method on parametrized domains is applied to approximate blood flow through an arterial bypass. The aim is to provide (a) a sensitivity analysis for relevant geometrical quantities of interest in bypass configurations and (b) rapid and re ...

2006