The search session has expired. Please query the service again.
The search session has expired. Please query the service again.
Displaying 21 –
40 of
105
We investigate well-structured graph-driven parity-FBDDs, which strictly generalize
the two well-known models parity OBDDs and well-structured graph-driven FBDDs.
The first main result is a characterization of the complexity of Boolean
functions represented by well-structured graph-driven parity-FBDDs in terms of
invariants of the function represented and the graph-ordering used.
As a consequence, we derive a lower bound criterion and prove an exponential
lower bound for certain linear code functions.
The...
A new implementation concept for parameterized specifications based on constructors and abstractors was recently introduced by Orejas, Navarro and Sánchez which includes most of the implementation concepts in the literature for initial as well as loose semantics. In this paper we redefine vertical and different kinds of horizontal compositions using the new concept of semi-pushout defined for a mixture of signature and specification morphisms. The main results concerning correctness of horizontal...
Computing the image of a regular language by the transitive closure of a relation is a central question in regular model checking. In a recent paper Bouajjani et al. [IEEE Comput. Soc. (2001) 399–408] proved that the class of regular languages – called APC – of the form
Computing the image of a regular language by the transitive closure of a
relation is a central question in regular model checking. In a recent
paper Bouajjani et al. [IEEE Comput. Soc. (2001) 399–408] proved that the class of
regular languages L – called APC – of the form UjL0,jL1,jL2,j...Lkj,j, where the union is finite and each
Li,j is either a single symbol or a language of the form B* with
B a subset of the alphabet, is closed under all semi-commutation
relations R. Moreover a recursive...
We provide an elementary proof of the fixpoint alternation hierarchy
in arithmetic, which in turn allows us to simplify the proof of the
modal mu-calculus alternation hierarchy. We further show that the
alternation hierarchy on the binary tree is strict, resolving a
problem of Niwiński.
Starting from late 90’s the public administration has started to employ a quite relevant amount of its budget in developing ICT solutions to better deliver services to citizens. In spite of this effort many statistics show that the mere availability of ICT based services does not guarantee per se their usage. Citizens have continued to largely access services through “traditional” means. In our study we suggest that the highlighted situation is partly due to the fact that relevant domain dependent...
Starting from late 90’s the public administration has started to employ a quite relevant
amount of its budget in developing ICT solutions to better deliver services to citizens.
In spite of this effort many statistics show that the mere availability of ICT based
services does not guarantee per se their usage. Citizens have continued to largely access
services through “traditional” means. In our study we suggest that the highlighted
situation is partly...
Floating-point arithmetic provides a fast but inexact way of
computing geometric predicates. In order for these predicates to be
exact, it is important to rule out all the numerical situations where
floating-point computations could lead to wrong results. Taking into
account all the potential problems is a tedious work to do by hand. We
study in this paper a floating-point implementation of a filter for the
orientation-2 predicate, and how a formal and partially automatized
verification of this...
Currently displaying 21 –
40 of
105