Foreword ICTCS 2010 special issue
Formal grammar for a fragment of the Serbian language
Formal language properties of hybrid systems with strong resets
We study hybrid systems with strong resets from the perspective of formal language theory. We define a notion of hybrid regular expression and prove a Kleene-like theorem for hybrid systems. We also prove the closure of these systems under determinisation and complementation. Finally, we prove that the reachability problem is undecidable for synchronized products of hybrid systems.
Formal language theory and the geometry of 3-manifolds.
Formal languages in dynamical systems
Formal Methods to Improve Public Administration Business Processes
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...
Formal Methods to Improve Public Administration Business Processes
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...
Formal Model of Activities As a Segment of Organizational Stock of Knowledge
Formal Specifications in Software Development: an Overview
Formal translation directed by parsing
Formalisation des connaissances pour la simulation du service-retour en tennis : le système lift
Dans cet article, nous présentons les aspects essentiels de la modélisation du processus décisionnel des joueurs de tennis dans une phase particulière de ce jeu sportif : le service-retour. Notre démarche se focalise sur la représentation des connaissances s'exerçant dans un continuum temporel scindé en micro-cycles et sur la construction de structures permettant d'envisager l'auto-apprentissage des caractéristiques technico-tactiques des joueurs par le système. Elle s'appuie sur la mise en oeuvre...
Formalization of Generalized Almost Distributive Lattices
Almost Distributive Lattices (ADL) are structures defined by Swamy and Rao [14] as a common abstraction of some generalizations of the Boolean algebra. In our paper, we deal with a certain further generalization of ADLs, namely the Generalized Almost Distributive Lattices (GADL). Our main aim was to give the formal counterpart of this structure and we succeeded formalizing all items from the Section 3 of Rao et al.’s paper [13]. Essentially among GADLs we can find structures which are neither V-commutative...
Formalization of Provenes fuzzy functional dependency in fuzzy databases.
In this paper we establish equivalence between a theory of fuzzy functional dependences and a fragment of fuzzy logic. We give a way to interpret fuzzy functional dependences as formulas in fuzzy logic. This goal is realized in a few steps. Truth assignment of attributes is defined in terms of closeness between two tuples in a fuzzy relation. A corresponding fuzzy formula is associated to a fuzzy functional dependence. It is proved that if a relation satisfies a fuzzy functional dependence, then...
Formalization of the Advanced Encryption Standard. Part I
In this article, we formalize the Advanced Encryption Standard (AES). AES, which is the most widely used symmetric cryptosystem in the world, is a block cipher that was selected by the National Institute of Standards and Technology (NIST) as an official Federal Information Processing Standard for the United States in 2001 [12]. AES is the successor to DES [13], which was formerly the most widely used symmetric cryptosystem in the world. We formalize the AES algorithm according to [12]. We then verify...
Formalized models of ontological systems
Formally certified floating-point filters for homogeneous geometric predicates
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...
Formulation and solution of the sequencing problem with parallel machines
Formulation of Cell Petri Nets
Based on the Petri net definitions and theorems already formalized in the Mizar article [13], in this article we were able to formalize the definition of cell Petri nets. It is based on [12]. Colored Petri net has already been defined in [11]. In addition, the conditions of the firing rule and the colored set to this definition, that defines the cell Petri nets are further extended to CPNT.i further. The synthesis of two Petri nets was introduced in [11] and in this work the definition is extended...
Formules sommatoires et systèmes de numération liés aux substitutions
Foundation of information retrieval.