| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2017
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 54:8, s. 789-818
-
Tidskriftsartikel (refereegranskat)
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Verification of heap manipulating programs with ordered data by extended forest automata
- 2016
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 53:4, s. 357-385
-
Tidskriftsartikel (refereegranskat)abstract
- We present a general framework for verifying programs with complex dynamic linked data structures whose correctness depends on ordering relations between stored data values. The underlying formalism of our framework is that of forest automata (FA), which has previously been developed for verification of heap-manipulating programs. We extend FA with constraints between data elements associated with nodes of the heaps represented by FA, and we present extended versions of all operations needed for using the extended FA in a fully-automated verification approach, based on abstract interpretation. We have implemented our approach as an extension of the Forester tool and successfully applied it to a number of programs dealing with data structures such as various forms of singly- and doubly-linked lists, binary search trees, as well as skip lists.
|
|
| 3. |
- Aceto, Luca, et al.
(författare)
-
A complete classification of the expressiveness of interval logics of Allen’s relations : the general and the dense cases
- 2016
-
Ingår i: Acta Informatica. - : Springer Science and Business Media LLC. - 0001-5903 .- 1432-0525. ; 53:3, s. 207-246
-
Tidskriftsartikel (refereegranskat)abstract
- Interval temporal logics take time intervals, instead of time points, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham’s modal logic of time intervals HS, which associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen’s interval relations). In this paper, we compare and classify the expressiveness of all fragments of HS on the class of all linear orders and on the subclass of all dense linear orders. For each of these classes, we identify a complete set of definabilities between HS modalities, valid in that class, thus obtaining a complete classification of the family of all 4096 fragments of HS with respect to their expressiveness. We show that on the class of all linear orders there are exactly 1347 expressively different fragments of HS, while on the class of dense linear orders there are exactly 966 such expressively different fragments.
|
|
| 4. |
- Aceto, L., et al.
(författare)
-
Lifting non-finite axiomatizability results to extensions of process algebras
- 2010
-
Ingår i: Acta Informatica. - Amsterdam : Elsevier. - 0001-5903 .- 1432-0525. ; 47:3, s. 147-177
-
Tidskriftsartikel (refereegranskat)abstract
- This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such reductions are translations between languages that preserve sound (in)equations and (in)equational provability over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown that prebisimilarity is not finitely based over CCS with the divergent process Ω, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity. This negative result is the inspiration for the development of a sharpened reduction method that is powerful enough to show that prebisimilarity is not finitely based over CCS with the divergent process Ω. © 2010 Springer-Verlag.
|
|
| 5. |
- Björklund, Henrik, et al.
(författare)
-
Conjunctive query containment over trees using schema information
- 2018
-
Ingår i: Acta Informatica. - : SPRINGER. - 0001-5903 .- 1432-0525. ; 55:1, s. 17-56
-
Tidskriftsartikel (refereegranskat)abstract
- We study the containment, satisfiability, and validity problems for conjunctive queries over trees with respect to a schema. We show that conjunctive query containment and validity are 2EXPTIME -complete with respect to a schema, in both cases where the schema is given as a DTD or as a tree automaton. Furthermore, we show that satisfiability for conjunctive queries with respect to a schema can be decided in NP . The problem is NP -hard already for queries using only one kind of axis. Finally, we consider conjunctive queries that can test for equalities and inequalities of data values. Here, satisfiability and validity are decidable, but containment is undecidable, even without schema information. On the other hand, containment with respect to a schema becomes decidable again if the "larger" query is not allowed to use both equalities and inequalities.
|
|
| 6. |
- Björklund, Johanna, 1961-, et al.
(författare)
-
Aggregation-based minimization of finite state automata
- 2021
-
Ingår i: Acta Informatica. - : Springer Nature. - 0001-5903 .- 1432-0525. ; 58, s. 177-194
-
Tidskriftsartikel (refereegranskat)abstract
- We present a minimization algorithm for non-deterministic finite state automata that finds and merges bisimulation-equivalent states. The bisimulation relation is computed through partition aggregation, in contrast to existing algorithms that use partition refinement. The algorithm simultaneously generalises and simplifies an earlier one by Watson and Daciuk for deterministic devices. We show the algorithm to be correct and run in time O(n2r2|Σ|), where n is the number of states of the input automaton M, r is the maximal out-degree in the transition graph for any combination of state and input symbol, and |Σ| is the size of the input alphabet. The algorithm has a higher time complexity than derivatives of Hopcroft’s partition-refinement algorithm, but represents a promising new solution approach that preserves language equivalence throughout the computation process. Furthermore, since the algorithm essentially computes the maximal model of a logical formula derived from M, optimisation techniques from the field of model checking become applicable.
|
|
| 7. |
- Carlsson, Svante, et al.
(författare)
-
On partitions and presortedness of sequences
- 1992
-
Ingår i: Acta Informatica. - 0001-5903 .- 1432-0525. ; 29:3, s. 267-280
-
Tidskriftsartikel (refereegranskat)abstract
- To take advantage of existing order in a sequence when sorting, we evaluate the quantity of this information by the minimal size of decomposition of the input sequence, particularly the minimal size of chain and of monotonic partitions. Some sorting strategies that are optimal with respect to these measures of presortedness are presented. The relationships between these new measures of presortedness and other known measures have also been explored. As an application, we carry out the optimality of an adaptive sorting algorithm Skiena'sMelsort. For some special partitioning strategies, we present two sorting algorithms based on Dijkstra'sSmoothsort. Moreover, the optimalities of these two algorithms are demonstrated. By examining the optimalities of sorting algorithms with respect to certain measures of presortedness, we also propose some optimal sorting strategies for one class of measures. Finally, we discuss other types of sorting problems, such as sorting multisets and topological sorting. In particular, we derive an optimal algorithm for sorting multisets and for finding the multiset sizes as well.
|
|
| 8. |
- Drewes, Frank, et al.
(författare)
-
Contextual Hyperedge Replacement
- 2015
-
Ingår i: Acta Informatica. - : Springer. - 0001-5903 .- 1432-0525. ; 52:6, s. 497-524
-
Tidskriftsartikel (refereegranskat)abstract
- Contextual hyperedge-replacement grammars (contextual grammars, for short) are an extension of hyperedge replacement grammars. They have recently been proposed as a grammatical method for capturing the structure of object-oriented programs, thus serving as an alternative to the use of meta-models like UML class diagrams in model-driven software design.In this paper, we study the properties of contextual grammars. Even though these grammars are not context-free, one can show that they inherit several of the nice properties of hyperedge replacement grammars. In particular, they possess useful normal forms and their membership problem is in NP.
|
|
| 9. |
- Drewes, Frank, et al.
(författare)
-
MAT learners for tree series : an abstract data type and two realizations
- 2011
-
Ingår i: Acta Informatica. - : Springer. - 0001-5903 .- 1432-0525. ; 48:3, s. 165-189
-
Tidskriftsartikel (refereegranskat)abstract
- We propose abstract observation tables, an abstract data type for learning deterministic weighted tree automata in Angluin’s minimal adequate teacher (MAT) model, and show that every correct implementation of abstract observation tables yields a correct MAT learner. Besides the “classical” observation table, we show that abstract observation tables can also be implemented by observation trees. The advantage of the latter is that they often require fewer queries to the teacher.
|
|
| 10. |
|
|
