Author name cluster
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.
Highlights Conference 2013 Conference Abstract
We extend the notion of invariant elementary definability to a variety of different graph representations, including those that strictly extend the power of first-order logic with an arbitrary linear order.
CSL Conference 2009 Conference Paper
Abstract For programs whose data variables range over boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this paper, we consider algorithmic verification of programs that use boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over a potentially unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace -complete for programs in which the array-accessing for -loops are not nested, (2) decidable for a restricted class of programs with doubly-nested loops. The second result establishes connections to automata and logics defining languages over data words.
CSL Conference 1996 Conference Paper
Abstract The Ordered conjecture of Kolaitis and Vardi asks whether fixed-point logic differs from first-order logic on every infinite class of finite ordered structures. In this paper, we develop the tool of bounded variable element types, and illustrate its application to this and the original conjectures of McColm, which arose from the study of inductive definability and infinitary logic on proficient classes of finite structures (those admitting an unbounded induction). In particular, for a class of finite structures, we introduce a compactness notion which yields a new proof of a ramified version of McColm's second conjecture. Furthermore, we show a connection between a model-theoretic preservation property and the Ordered Conjecture, allowing us to prove it for classes of strings (colored orderings). We also elaborate on complexity-theoretic implications of this line of research.
I&C Journal 1988 Journal Article
We consider programs that accept descriptions of inductive inference problems and return machines that solve them. Several design specifications for synthesizers of this kind are considered from a recursion-theoretic perspective.
IJCAI Conference 1983 Conference Paper