enter search term and/or author name
Refining the Process Rewrite Systems Hierarchy via Ground Tree Rewrite Systems
Stefan Göller, Anthony Widjaja Lin
Article No.: 26
In his seminal paper, Mayr introduced the well-known process rewrite systems (PRS) hierarchy, which contains many well-studied classes of infinite-state systems including pushdown systems (PDS), Petri nets, and PA-processes. A separate development...
Recently, there has been an effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions.
At the heart of quantitative...
Identifying Efficient Abductive Hypotheses Using Multicriteria Dominance Relation
Maciej Komosinski, Adam Kups, Dorota Leszczyńska-Jasion, Mariusz Urbański
Article No.: 28
In this article, results of the automation of an abductive procedure are reported. This work is a continuation of our earlier research [Komosinski et al. 2012], where a general scheme of the procedure has been proposed. Here, a more advanced...
The Ordering Principle in a Fragment of Approximate Counting
Albert Atserias, Neil Thapen
Article No.: 29
The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the...
In the past years, the adoption of adaptive systems has increased in many fields of computer science, such as databases and software engineering. These systems are able to automatically react to events by collecting information from the external...
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
Gerhard Schellhorn, John Derrick, Heike Wehrheim
Article No.: 31
Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small...
Terminating Evaluation of Logic Programs with Finite Three-Valued Models
Fabrizio Riguzzi, Terrance Swift
Article No.: 32
As evaluation methods for logic programs have become more sophisticated, the classes of programs for which termination can be guaranteed have expanded. From the perspective of ar set programs that include function symbols, recent work has...
Inference of Field-Sensitive Reachability and Cyclicity
Damiano Zanardini, Samir Genaim
Article No.: 33
In heap-based languages, knowing that a variable x points to an acyclic data structure is useful for analyzing termination. This information guarantees that the depth of the data structure to which x points is greater than the depth of the...
Reasoning About Strategies: On the Model-Checking Problem
Fabio Mogavero, Aniello Murano, Giuseppe Perelli, Moshe Y. Vardi
Article No.: 34
In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution...
Barbed bisimilarity is a widely used behavioral equivalence for interactive systems: given a set of predicates (denoted “barbs” and representing basic observations on states) and a set of contexts (representing the possible execution...