Author name cluster

Constantin Enea

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

I&C Journal 2018 Journal Article

On reducing linearizability to state reachability

Ahmed Bouajjani
Michael Emmi
Constantin Enea
Jad Hamza

Efficient implementations of atomic objects such as concurrent stacks and queues are especially susceptible to programming errors, and necessitate automatic verification. Unfortunately their correctness criteria – linearizability with respect to given ADT specifications – are hard to verify. Even on classes of implementations where the usual temporal safety properties like control-state reachability are decidable, linearizability is undecidable. In this work we demonstrate that verifying linearizability for certain fixed ADT specifications is reducible to control-state reachability, despite being harder for arbitrary ADTs. We effectuate this reduction for several of the most popular atomic objects. This reduction yields the first decidability results for verification without bounding the number of concurrent threads. Furthermore, it enables the application of existing safety-verification tools to linearizability verification.

Details DOI

I&C Journal 2017 Journal Article

On the path-width of integer linear programming

Constantin Enea
Peter Habermehl
Omar Inverso
Gennaro Parlato

We consider the feasibility problem of integer linear programming (ILP). We show that solutions of any ILP instance can be naturally represented by an FO-definable class of graphs. For each solution there may be many graphs representing it. However, one of these graphs is of path-width at most 2n, where n is the number of variables in the instance. Since FO is decidable on graphs of bounded path-width, we obtain an alternative decidability result for ILP. The technique we use underlines a common principle to prove decidability which has previously been employed for automata with auxiliary storage. We also show how this new result links to automata theory and program verification.

Details DOI

GandALF Workshop 2014 Workshop Paper

On the Path-Width of Integer Linear Programming

Constantin Enea
Peter Habermehl
Omar Inverso
Gennaro Parlato

We consider the feasibility problem of integer linear programming (ILP). We show that solutions of any ILP instance can be naturally represented by an FO-definable class of graphs. For each solution there may be many graphs representing it. However, one of these graphs is of path-width at most 2n, where n is the number of variables in the instance. Since FO is decidable on graphs of bounded path- width, we obtain an alternative decidability result for ILP. The technique we use underlines a common principle to prove decidability which has previously been employed for automata with auxiliary storage. We also show how this new result links to automata theory and program verification.

PDF Details DOI

TARK Conference 2013 Conference Paper

Model checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

Rodica Bozianu
Catalin Dima
Constantin Enea

We identify a subproblem of the model-checking problem for the epistemic µ-calculus which is decidable. Formulas in the instances of this subproblem allow free variables within the scope of epistemic modalities in a restricted form that avoids embodying any form of common knowledge. Our subproblem subsumes known decidable fragments of epistemic CT L/LT L, may express winning strategies in two-player games with one player having imperfect information and non-observable objectives, and, with a suitable encoding, decidable instances of the model-checking problem for AT LiR. 1.

Details

GandALF Workshop 2010 Workshop Paper

Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions

Cătălin Dima
Constantin Enea
Dimitar Guelev

We present a variant of ATL with distributed knowledge operators based on a synchronous and perfect recall semantics. The coalition modalities in this logic are based on partial observation of the full history, and incorporate a form of cooperation between members of the coalition in which agents issue their actions based on the distributed knowledge, for that coalition, of the system history. We show that model-checking is decidable for this logic. The technique utilizes two variants of games with imperfect information and partially observable objectives, as well as a subset construction for identifying states whose histories are indistinguishable to the considered coalition.

PDF Details DOI