 |
 |
Volume 3, Issue 1
2007
1. Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
We consider Dense-Timed Petri Nets (TPN), an extension of Petri nets in which each token is equipped with a real-valued clock and where the semantics is lazy (i.e., enabled transitions need not fire; time can pass and disable transitions). We consider the following verification problems for TPNs. (i) Zenoness: whether there exists a zeno-computation from a given marking, i.e., an infinite computation which takes only a finite amount of time. We show decidability of zenoness for TPNs, thus solving an open problem from [Escrig et al.]. Furthermore, the related question if there exist arbitrarily fast computations from a given marking is also decidable. On the other hand, universal zenoness, i.e., the question if all infinite computations from a given marking are zeno, is undecidable. (ii) Token liveness: whether a token is alive in a marking, i.e., whether there is a computation from the marking which eventually consumes the token. We show decidability of the problem by reducing it to the coverability problem, which is decidable for TPNs. (iii) Boundedness: whether the size of the reachable markings is bounded. We consider two versions of the problem; namely semantic boundedness where only live tokens are taken into consideration in the markings, and syntactic boundedness where also dead tokens are considered. We show undecidability of semantic boundedness, while we prove that syntactic boundedness is decidable through an extension of the Karp-Miller algorithm.
2. Cores of Countably Categorical Structures
A relational structure is a core, if all its endomorphisms are embeddings. This notion is important for computational complexity classification of constraint satisfaction problems. It is a fundamental fact that every finite structure has a core, i.e., has an endomorphism such that the structure induced by its image is a core; moreover, the core is unique up to isomorphism. Weprove that every \omega -categorical structure has a core. Moreover, every \omega-categorical structure is homomorphically equivalent to a model-complete core, which is unique up to isomorphism, and which is finite or \omega -categorical. We discuss consequences for constraint satisfaction with \omega -categorical templates.
3. Expressiveness of Metric modalities for continuous time
We prove a conjecture by A. Pnueli and strengthen it showing a sequence of "counting modalities" none of which is expressible in the temporal logic generated by the previous modalities, over the real line, or over the positive reals. Moreover, there is no finite temporal logic that can express all of them over the real line, so that no finite metric temporal logic is expressively complete.
4. Logic Meets Algebra: the Case of Regular Languages
The study of finite automata and regular languages is a privileged meeting point of algebra and logic. Since the work of Buchi, regular languages have been classified according to their descriptive complexity, i.e. the type of logical formalism required to define them. The algebraic point of view on automata is an essential complement of this classification: by providing alternative, algebraic characterizations for the classes, it often yields the only opportunity for the design of algorithms that decide expressibility in some logical fragment. We survey the existing results relating the expressibility of regular languages in logical fragments of MSO[S] with algebraic properties of their minimal automata. In particular, we show that many of the best known results in this area share the same underlying mechanics and rely on a very strong relation between logical substitutions and block-products of pseudovarieties of monoid. We also explain the impact of these connections on circuit complexity theory.
5. Predicate Abstraction with Under-approximation Refinement
We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require an abstract transition relation to be generated, but instead executes the concrete transitions while storing abstract versions of the concrete states, as specified by a set of abstraction predicates. For each explored transition the method checks, with the help of a theorem prover, whether there is any loss of precision introduced by abstraction. The results of these checks are used to decide termination or to refine the abstraction by generating new abstraction predicates. If the (possibly infinite) concrete system under analysis has a finite bisimulation quotient, then the method is guaranteed to eventually explore an equivalent finite bisimilar structure. We illustrate the application of the approach for checking concurrent programs.
6. Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning
In Verification and in (optimal) AI Planning, a successful method is to formulate the application as boolean satisfiability (SAT), and solve it with state-of-the-art DPLL-based procedures. There is a lack of understanding of why this works so well. Focussing on the Planning context, we identify a form of problem structure concerned with the symmetrical or asymmetrical nature of the cost of achieving the individual planning goals. We quantify this sort of structure with a simple numeric parameter called AsymRatio, ranging between 0 and 1. We run experiments in 10 benchmark domains from the International Planning Competitions since 2000; we show that AsymRatio is a good indicator of SAT solver performance in 8 of these domains. We then examine carefully crafted synthetic planning domains that allow control of the amount of structure, and that are clean enough for a rigorous analysis of the combinatorial search space. The domains are parameterized by size, and by the amount of structure. The CNFs we examine are unsatisfiable, encoding one planning step less than the length of the optimal plan. We prove upper and lower bounds on the size of the best possible DPLL refutations, under different settings of the amount of structure, as a function of size. We also identify the best possible sets of branching variables (backdoors). With minimum AsymRatio, we prove exponential lower bounds, and identify minimal backdoors of size linear in the number of variables. With maximum AsymRatio, […]
7. Real-Time Model-Checking: Parameters everywhere
In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). Our results are as follows. On the negative side, we show that the model-checking problem of TCTL extended with parameters is undecidable over discrete-timed automata with only one parametric clock. The undecidability result needs equality in the logic. On the positive side, we show that the model-checking and the parameter synthesis problems become decidable for a fragment of the logic where equality is not allowed. Our method is based on automata theoretic principles and an extension of our method to express durations of runs in timed automata using Presburger arithmetic.
8. On the decidability and complexity of Metric Temporal Logic over finite words
Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL--which includes invariance and time-bounded response properties--is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature.
9. Adventures in time and space
This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR, has its first-order programs characterize the polynomial-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR-types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of polynomial-time. The time-restricting part is an affine version of Barber and Plotkin's DILL. Two semantics are constructed for ATR. The first is a pruning of the naive denotational semantics for ATR. This pruning removes certain functions that cause otherwise feasible forms of recursion to go wrong. The second semantics is a model for ATR's time complexity relative to a certain abstract machine. This model provides a setting for complexity recurrences arising from ATR recursions, the solutions of which yield second-order polynomial time bounds. The time-complexity semantics is also shown to be sound relative to the costs of interpretation on the abstract machine.