| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Universality Analysis for One-Clock Timed Automata
- 2008
-
Ingår i: Fundamenta Informaticae. - 0169-2968 .- 1875-8681. ; 89:4, s. 419-450
-
Tidskriftsartikel (refereegranskat)abstract
- This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if epsilon-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.
|
|
| 2. |
- Doherty, Patrick, et al.
(författare)
-
A correspondence framework between three-valued logics and similarity-based approximate reasoning
- 2007
-
Ingår i: Fundamenta Informaticae. - : IOS Press. - 0169-2968 .- 1875-8681. ; 75:1-4, s. 179-193
-
Tidskriftsartikel (refereegranskat)abstract
- This paper focuses on approximate reasoning based on the use of similarity spaces. Similarity spaces and the approximated relations induced by them are a generalization of the rough set-based approximations of Pawlak [17, 18]. Similarity spaces are used to define neighborhoods around individuals and these in turn are used to define approximate sets and relations. In any of the approaches, one would like to embed such relations in an appropriate logic which can be used as a reasoning engine for specific applications with specific constraints. We propose a framework which permits a formal study of the relationship between approximate relations, similarity spaces and three-valued logics. Using ideas from correspondence theory for modal logics and constraints on an accessibility relation, we develop an analogous framework for three-valued logics and constraints on similarity relations. In this manner, we can provide a tool which helps in determining the proper three-valued logical reasoning engine to use for different classes of approximate relations generated via specific types of similarity spaces. Additionally, by choosing a three-valued logic first, the framework determines what constraints would be required on a similarity relation and the approximate relations induced by it. Such information would guide the generation of approximate relations for specific applications.
|
|
| 3. |
- Drewes, Frank, et al.
(författare)
-
Path languages of random permitting context tree grammars are regular
- 2008
-
Ingår i: Fundamenta Informaticae. - Amsterdam : IOS Press. - 0169-2968 .- 1875-8681. ; 82:1-2, s. 47-60
-
Tidskriftsartikel (refereegranskat)abstract
- The path languages of random permitting context tree languages are investigated. The main result is that these path languages are regular. This confirms a previous conjecture.
|
|
| 4. |
- Högberg, Johanna, 1978-, et al.
(författare)
-
Bisimulation mimisation of weighted automata on unranked trees
- 2009
-
Ingår i: Fundamenta Informaticae. - Poland : Polish mathematical society. - 0169-2968 .- 1875-8681. ; 92:1-2, s. 103-130
-
Tidskriftsartikel (refereegranskat)abstract
- Several models of automata are available that operate unranked trees. Two well-known examples are the stepwise unranked tree automaton (suta) and the parallel unranked tree automaton (puta). By adding a weight, taken from some semiring, to every transition we generalise these two qualitative automata models to quantitative models, thereby obtaining weighted stepwise unranked tree automata (wsuta) and weighted parallel unranked tree automata (wputa); the qualitative automata models are reobtained by choosing the BOOLEAN semiring. The weighted versions have applications in natural language processing, XML-based data management and quantitative information retrieval. We address the minimisation problem of wsuta and wputa by using (forward and backward) bisimulations and we prove the following results: (1) for every wsuta an equivalent forward (resp. backward) bisimulation minimal wsuta can be computed in time O(mn) where n is the number of states and m is the number of transitions of the given wsuta; (2) the same result is proved for wputa instead of wsuta; (3) if the semiring is additive cancellative or the BOOLEAN semiring, then the bound can be improved to O(mlog n) for both wsuta and wputa; (4) for every deterministic puta we can compute a minimal equivalent deterministic puta in time O(mlog n); (5) the automata models wsuta, wputa, and weighted unranked tree automaton have the same computational power.
|
|
| 5. |
- Seceleanu, Tiberiu, et al.
(författare)
-
Modeling Communication with Synchronized Environments
- 2008
-
Ingår i: Fundamenta Informaticae. - 0169-2968 .- 1875-8681. ; 86:3, s. 343-369
-
Tidskriftsartikel (refereegranskat)abstract
- A deterministic behavior of systems composed of several modules is a desirable design goal. Assembling a complex system from components requires also a high degree of re-usability. The compatibility of the selected components may become a problem even at abstract design levels, due to possible different degrees of model determinacy, possible different execution models, etc. In this cases, an overall deterministic system behavior is difficult to achieve. The development of communication mechanisms between such components will have then to accommodate the differences, so that both correct processing and information exchange (data and control, appropriate choices and relative timing or sequencing) are achieved. For instance, human-machine interaction offers a good example of cooperation between deterministic models (machines) communicating with highly non-deterministic counterparts (the human models, if not restricted). We analyze here such communication mechanisms by "confronting" synchronized and un-synchronized models of execution, in the framework of action systems, a state based formalism. We "force" the two models to coexist within the same context and explore the possibilities of building trustworthy communication channels between them. We base our approach on a combined polling - interrupt scheme, which allows us to mitigate communication issues that may otherwise compromise the correct input-output system behavior. More robust system models are obtained by applying specific correctness rules of refinement. We illustrate our methods on an audio system example, implementable as either a software or a hardware device.
|
|
| 6. |
- Vitoria, Aida, et al.
(författare)
-
Modelling and Reasoning with Paraconsistent Rough Sets
- 2009
-
Ingår i: Fundamenta Informaticae. - 0169-2968 .- 1875-8681. ; 97:4, s. 405-438
-
Tidskriftsartikel (refereegranskat)abstract
- We present a language for defining paraconsistent rough sets and reasoning about them. Our framework relates and brings together two major fields: rough sets [23] and paraconsistent logic programming [9]. To model inconsistent and incomplete information we use a four-valued logic. The language discussed in this paper is based on ideas of our previous work [21, 32, 22] developing a four-valued framework for rough sets. In this approach membership function, set containment and set operations are four-valued, where logical values are t (true), f (false), i (inconsistent) and u (unknown). We investigate properties of paraconsistent rough sets as well as develop a paraconsistent rule language, providing basic computational machinery for our approach.
|
|
| 7. |
- Abel, Andreas, 1974, et al.
(författare)
-
Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs
- 2007
-
Ingår i: Fundamenta Informaticae. - 0169-2968. ; 77:4, s. 345-395
-
Tidskriftsartikel (refereegranskat)abstract
- Martin-Löf's Logical Framework is extended by strong Sigma-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped beta eta-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with eta-equality on beta-normal forms, which is shown equivalent to the algorithmic equality.
|
|
| 8. |
- Coquand, Thierry, 1961
(författare)
-
The completeness of typing for context-semantics
- 2007
-
Ingår i: Fundamenta Informaticae. - 0169-2968. ; 77:4, s. 293-301
-
Tidskriftsartikel (refereegranskat)abstract
- We present a variation of Hindley's completeness theorem for simply typed lambda-calculus. It is based on a Kripke semantics where the worlds are contexts, called context-semantics. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic lambda-calculus [2]. We relate in this way works done in proof theory [4, 14] with a fundamental result in lambda-calculus.
|
|
