Technical reports |
|
TR12-02 (2012) - Importance Sampling using Rényi divergence We present an alternative approach to the problem of estimating probabilities of rare events and for optimization problems using the class of Rényi divergences of order α > 1. The general procedure we describe does not involve any specific family of distributions, the only restriction is that the search space consists of product form probability density functions. We discuss an algorithm for estimation of probability of rare events and a version for continuous optimization. The results of numerical experimentation with these algorithms carried in the last section support their performances. Full document: PDF | BibTeX entry TR12-01 (2012) - Importance Resampling with MRAS algorithm for Bermudan option pricing In this paper we investigate a MRAS type algorithm for pricing Bermudan option. We use three different model for the price dynamics: geometric Brownian, Merton jump-diffusion and a relative new one, namely, the double asymmetric exponentially jump-diffusion model. Although MRAS procedure includes a form of importance sampling we modify the original procedure in order to implement a sampling importance resampling in two different ways. The numerical results show that both resampling methods give better results, and that using the reference distributions is almost twice as fast as MRAS and very reliable offering small confidence intervals. Full document: PDF | BibTeX entry TR11-01 (2011) - Learning to unlearn in lattices of concepts: A case study in Fluid Construction Grammars
This report outlines a couple of lattice-based (un)learning strategies proposed in a recent development of unification-based grammars, namely the Fluid Construction Grammar (FCG) setup. These (un)learning strategies are inspired by two linguistic phenomena occurring in a dialect spoken in the Banat area of Romania. Children from that region - where influences produced over centuries by Serbian, a Slavic language, are obvious - learn in school the modern Romanian language, which is a Romance language. This particular setup offers us the possibility to model in FCG a two-step learning process: the first step is that of learning a (perfective) verbal aspect similar to the one already presented by Kateryna Gerasymova in her MSc thesis, while the second one is concerned with un-learning (or, learning another linguistic "construction" over) this verbal aspect. Thus, the interesting issue here is how learning could continue beyond learning the verbal aspects. We will first give linguistic facts, after which we will outline the way in which FCG could model such a linguistic process. From the computational point of view, we show that the heuristics used in this grammar repairing process can be automatically derived since the meanings associated to words and phrases are organized in a lattice of feature structures, according to the underlying constraint logics. We will later discuss the case of another verbal marker in the dialect spoken in Banat. It will lead us to sketch a composite, quite elaborated (un)learning strategy. Full document: PDF | BibTeX entry TR10-05 (2010) - Automating Coinduction with Case Analysis Coinduction is a major technique employed to prove behavioral properties of systems, such as behavioral equivalence. Its automation is highly desirable, despite the fact that most behavioral problems are $\Pi_2^0$-complete. Circular coinduction, which is at the core of the CIRC prover, automates coinduction by systematically deriving new goals and proving existing ones until, hopefully, all goals are proved. Motivated by practical examples, circular coinduction and CIRC have been recently extended with several features, such as special contexts, generalization and simplification. Unfortunately, none of these extensions eliminates the need for case analysis and, consequently, there are still many natural behavioral properties that CIRC cannot prove automatically. This paper presents an extension of circular coinduction with case analysis constructs and reasoning, as well as its implementation in CIRC. To uniformly prove the soundness of this extension, as well as of past and future extensions of circular coinduction and CIRC, this paper also proposes a general correct-extension technique based on equational interpolants. Full document: PDF | BibTeX entry TR10-04 (2010) - Languages attached to Parikh Matrices This report presents an approach of formal languages based on Parikh matrices. We will display several points of characterizing various aspects of languages using Parikh matrices and the Parikh matrix mapping. The results included in this report are mainly obtained in [Atanasiu, R., 2010]. Full document: PDF | BibTeX entry TR10-03 (2010) - Applications of Parikh Matrices in Coding Theory In this report we will describe a possible application of Parikh matrices and amiability in the field of information security. The results presented were developed in [Atanasiu, A. & Atanasiu, R., 2008]. Full document: PDF | BibTeX entry TR10-02 (2010) - FCGlight: Making the bridge between Fluid Construction Grammars and main-stream unification grammars by using feature constraint logics
Fluid Construction Grammars (FCGs) are a flavour of Construction Grammars, which themselves are unification-based grammars. Its syntax is (only) up to certain extent similar to other unification-based grammars. However, it lacks a declarative semantics, while its procedural semantics is truly particular, compared to other unification-based grammar formalisms. Here we propose the re-definition of a subset of the FCG formalism (henceforth called FCGlight) within the framework of (order-sorted) feature constraint logics (OSF-logic) that would assign FCG a rigorous (both declarative a and procedural) semantics, which is suitable for both parsing, generation and grammar learning. In this way we will be able to compare FCG to other unification-based grammars. We will also get the advantage of associating it another classical paradigm for learning ("evolving") new grammars. This is learning in hierarchies (lattices) of concepts which exploits a partial order relation (generalisation / specialisation) between grammars, instead of the method currently used by FCG, which is (inspired by) reinforcement learning. This will enable a rather natural link with the linguistic background knowledge when devising the grammar repair strategies and a clear way to compare different grammars that could be learned by an agent at each step during the grammar evolution process. In return, inspired by the FCG approach to grammar learning, we are able to define new ways for learning grammars in other unification-based formalisms. In particular, ILP-like learning of HPSGs can be substantially improved by using ideas borrowed from FCG:- instead of using a given "golden" test suite (against which the learning is performed), this test suite is dynamically produced during the language game (played by two agents); - the grammar learning process will be "grounded", something which was not considered before; - we will learn also new rules (instead of modifying the given ones, as currently done in ilpLIGHT) - learning new rules by generalising upon already learned rules, will also be a significant step forward. Full document: PDF | BibTeX entry TR10-01 (2010) - Yet Another SVM for MiRNA Recognition: yasMiR We designed a new SVM for microRNA identification, whose novelty is two-folded: firstly many of its features incorporate the base-pairing probabilities provided by McCaskill's algorithm, and secondly the classification performance is improved by using a certain similarity ("profile"- based) measure between the training and test microRNAs and a set of carefully chosen ("pivot") RNA sequences. Comparisons with some of the best existing SVMs for microRNA identification prove that our SVM obtains truly competitive results. Full document: PDF | BibTeX entry TR09-04 (2009) - Ontology-Based Modeling and Recommendation Techniques for Adaptive Hypermedia Systems Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR09-03 (2009) - Time Constraints in Workflow Net Theory Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR09-02 (2009) - Textual Entailment Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR09-01 (2009) - Securing the Media Stream Inside VoIP SIP Based Sessions One of the main issues encountered in the development of VoIP applications and infrastructures relates with ensuring the security of the communication channel between peers. The discussion on this subject can be split in two principal directions: the signaling path security and the media path security. In this document we focus on the latter by overviewing the current most important available mechanisms and their way of interworking for architectures based on one of the most deployed standards in VoIP communication - Session Initiaton Protocol (SIP). Full document: PDF | BibTeX entry TR08-03 (2008) - Learning to Unroll Loops Optimally Every few months new types of hardware are released. Compiler writers face the challenging task of keeping the compiler optimizations up-to-date with the latest in hardware technology. In this paper we apply machine learning techniques to predict the best unroll factors for loops, using GCC and the x86 architecture for our experiments. We show that, depending on the machine learning tools used, we get similar or slightly better performance than the native GCC loop optimizer. Our result shows that machine learning techniques can be used to automatically train the heuristic that computes the unroll factor for loops, saving time for compiler manufacturers and providing better performance in the case of scientific computations. Full document: PDF | BibTeX entry TR08-02 (2008) - A Rewrite Stack Machine for ROC! ROC! is a deterministic rewrite strategy language which includes the rewrite rules as basic operators, and the deterministic choice and the repetition as high-level strategy operators. In this paper we present a method which, for a given term rewriting system (TRS) R, constructs a new TRS R' such that R'-rewriting is equivalent (sound and complete) with R-rewriting constrained by ROC!. Since R' uses a stack, it is called a rewrite stack machine. Full document: PDF | BibTeX entry TR08-01 (2008) - Support Vector Machines for MicroRNA Identification This technical report provides an overview on the support vector machines that have been designed during the recent years for the identification of microRNA sequences. Our aim is to arrive in the end to identify potential ways in which the quality of such machine learning methods could be further improved, knowing that the rate of false positves they produce is still too high. Full document: PDF | BibTeX entry TR07-02 (2007) - Secrecy for Security Protocols Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR07-01 (2007) - Secret Sharing Schemes with Applications in Security Protocols Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR06-01 (2006) - Strategies and Tactics in Operational Semantics
We refer to strategies setting the objective of a computation step rather than to evaluation strategies (as eager or lazy evaluations). We use these strategies to define semantics of a system starting from its elementary operational entities, and then combining them. The tactics of a strategy are given by rewriting steps. While a strategy is at a higher level and defines "what is the goal" of a computation, the tactics are at a lower level and tell "how it is possible to reach the goal". We use rewriting systems as a general model of computing. In this framework we give an operational semantics of the strategic transitions in terms of tactical rewritings. The approach is inspired by a new model of computation given by membrane systems. We define the strategy semantics for membrane systems involving the maximal parallel rewriting and priorities. We show that strategies are not powerful enough to define alone the semantics of membrane systems involving promoters. This is possible when we encode the state of the membrane in a richer structure. Full document: PDF | BibTeX entry TR05-07 (2005) - Embedding mobile ambients into the pi-calculus The mobile ambient paradigm of mobile computations is very expressive and allows various embeddings into it of other models of computations such as Turing machine, the lambda-calculus, and the pi-calculus. In this paper we demonstrate that we have a closer relationship between mobile ambients and the pi-calculus. We present an embedding of pure mobile ambients into a fragment of the pi-calculus, namely the localized sum-free synchronous monadic pi-calculus with matching and mismatching. The embedding is achieved by associating a pair of localized pi-terms Structure_A and Ruler to every mobile ambient A. Structure_A simulates the spatial structure of A by means of communication channels. Ruler is a universal pi-process intended to simulate the operational semantics of the mobile ambients. This embedding of pure mobile ambients into a subset of the pi-calculus opens new ways to the analysis of ambients by means of techniques used in the pi-calculus. Full document: PDF | BibTeX entry TR05-06 (2005) - A Comparative Study on Feature Selection Algorithms in Data Mining
The field of feature selection in data mining has experienced a great development in the past few years. Unfortunately, there are few works that show a comparative analysis of feature selection algorithms introduced until now. In this technical report we analyze the effect that feature selection has on the performance of five learning algorithms. We use nine of the most known feature selection algorithms. We conduct our study on two classification problems, Dermatology and Zoo, whose datasets are provided in the UCI (University of California at Irvine) repository. We realize a comparative study on the effects that the chosen feature selection algorithms have on the performance and the running time of the learning algorithms used in solving the two problems. On these problems, the feature selection algorithms provide an accuracy which is 1.09% and respectively 1.98% higher than the accuracy obtained by learning algorithms alone. Additionally, the reduction of running time especially for time consuming learning algorithms like SVMO is highly significant, 59% and respectively 91%. Full document: PS | BibTeX entry TR05-05 (2005) - Threshold RSA Based on the General Chinese Remainder Theorem In threshold (or group-oriented) cryptography the capacity of performing cryptographic operations such as decryption or digital signature generation is shared among members of a certain group. This can be achieved by combining multiplicative secret sharing schemes with homomorphic cryptographic operations. In this paper we focus on threshold RSA decryption and threshold RSA digital signature generation. More exactly, we combine the threshold secret sharing schemes based on the Chinese remainder theorem with the RSA cryptosystem, as an alternative to the classical solutions based on the Shamir's threshold secret sharing scheme. Full document: PS | BibTeX entry TR05-04 (2005) - Walking the Royal Road with Integrated-Adaptive Genetic Algorithms The aim of this paper is to show that exploiting knowledge extracted from the optimization process is important for the success of an evolutionary solver. In the context of NK fitness landscapes, we identify two causes for the difficulty of an optimization problem: the intrinsic combinatorial difficulty and the random-search hybridization. We apply these concepts for the royal road fitness landscape. Experimental results indicate that Integrated-Adaptive Genetic Algorithms (IAGA) are particularly suited for tackling randomsearch hybridization. A learn-as-you-go system aimed at a fine-grained adaptation of operators behavior increases the solving power and convergence speed of IAGA. We conclude that the royal road problem is actually being "royal" for the traditional GA, but for a class of adaptive genetic algorithms. Full document: PDF | BibTeX entry TR05-03 (2005) - An Ordering-Based Genetic Approach to Graph Coloring We introduce a new evolutionary formulation of the graph coloring problem, based on the interplay between orderings and colorings of vertices. The new formulation aims at breaking the symmetry in the solution space and provides opportunities for combining evolutionary and other search techniques. Our formulation is very simple compared to previous approaches which use the relationship between a graph's chromatic number and its acyclic orientations. We have experimented on graphs from the DIMACS Computational Challenge. The results provide evidence that the ordering approach can be used to obtain accurate colorings. We also give a general property which accounts for the computational difficulty of all approaches that attempt to iteratively reduce the number of colors in a coloring. Full document: PDF | BibTeX entry TR05-02 (2005) - Decidability and Complexity Results for Security Protocols Security protocols are prescribed sequences of interactions between entities designed to provide various security services across distributed systems. Security protocols are often wrong due to the extremely subtle properties they are supposed to ensure. Deciding whether or not a security protocol assures secrecy is one of the main challenge in this area. In this paper we survey the most important decidability and complexity results regarding the secrecy problem for various classes of security protocols, such as bounded protocols, finite-sessions protocols, normal protocols, and tagged protocols. All the results are developed under the same formalism. Several flawed statements claimed in the literature are corrected. Simplified proofs and reductions, as well as slight extensions of some known results, are also provided. Full document: PDF | BibTeX entry TR05-01 (2005) - Web Ontology Verification and Analysis in the Z Framework The correctness of Web ontologies and data is an important aspect in the development of reliable Semantic Web systems. Software specification and verification tools can be used to complement the Knowledge Representation tools in reasoning about Semantic Web. The key for applying software verification tools to Semantic Web is to develop the sound transformation techniques from Web ontology to software specification models so that the associated verification tools can be applied to check the transformed specification models. Our previous work has demonstrated a practical approach to translating Web ontologies to Z specification models. However, from a sound engineering point of view, the translation is lacking the theoretical work that can formally relate the respective underlying logical systems in semantic web and Z. In this paper, we show that the logics underlying OWL, SWRL, and SWRL FOL can be represented as institutions, we investigate the properties of these institutions, and we show that the institution comorphism provides a formal semantic foundation for encoding web ontologies specifications in Z. Full document: PS | BibTeX entry TR04-04 (2004) - Proprietati structurale ale retelelor Petri Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR04-03 (2004) - Modular Analysis of Petri Net Models Thesis submitted to the ``Alexandru Ioan Cuza'' University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science. Full document: PDF | BibTeX entry TR04-02 (2004) - Invariants and Verification of Properties for Jumping Petri Nets This paper presents the notions of place and transition invariants for jumping Petri nets, and the results concerning invariants extended to them from classical Petri nets. Moreover, it presents some examples of systems modelled by jumping Petri nets and the verification of their properties using the invariant method. Full document: PS | BibTeX entry TR04-01 (2004) - ADF - Abstract Framework for Developing Mobile Agents In this technical report, the authors propose an abstract framework, called ADF (Agent Developing Framework), to be used in designing and implementation stages of building (mobile) agents within a multi-agent architecture. We also investigate the possibility of developing, in a generic manner, different components to be integrated into agent applications. The ADF framework consists of a hierarchy of classes (structured as a Java package) and a visual developing tool. The proposed API offers the core functionalities of an agent-oriented system (e.g., agents, hosts, name service, migration, and messaging). Full document: PDF | BibTeX entry TR03-06 (2003) - Structuri de accesibilitate reduse pentru retele Petri de nivel inalt Aceasta lucrare prezinta o sinteza asupra structurilor de accesibilitate si de acoperire, precum si a aplicatiilor acestora, pentru retele Petri de nivel inalt. Full document: PS | BibTeX entry TR03-05 (2003) - Specification and Verification of Synchronized Concurrent Objects Hidden algebra is used to specify object systems, and CCS is used to describe synchronous concurrent systems. We introduce a new specification formalism which we call hiddenCCS, formed by extending the object specification with synchronization elements related to the invocation of complementary methods in different object components, and using a CCS coordinating module able to describe the interaction patterns of method invocations. Various results refer to strong bisimulation over the hiddenCCS configurations. We show that weak bisimulation allows for specification development by stepwise refinement. We investigate how the existing tools CWB, BOBJ, Maude can be integrated to describe and verify useful properties of the synchronized concurrent objects. The hiddenCCS specifications can be described in the rewriting logic of Maude. Finally we present the first steps towards a new CTL verification tool for hiddenCCS. A concise and revised version of the paper was accepted at the Fourth International Conference on Integrated Formal Methods (IFM2004) . Full document: PS | BibTeX entry TR03-04 (2003) - Incremental Counting Satisfiability for Real-Time Systems Counting the number of truth assignments in a propositional formula has a number of applications, including the verification of timing constraints for real-time specification. This number can tell us how "far away" is a given specification from satisfying its safety assertion. However, specifications and safety assertions are often modified in an incremental fashion, where problematic bugs are fixed one at a time. To mirror such changes, we propose an incremental algorithm for counting satisfiability. Our proposed incremental algorithm is optimal as no unnecessary nodes are created during each incremental counting. To illustrate this application, we show how incremental satisfiability counting can be applied to a well-known rail-road crossing example, when its specification is being modified. A concise and revised version of the paper was accepted at the 10th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2004). Full document: PS | BibTeX entry TR03-03 (2003) - Behavioral Bisimulation and CTL Models for Hidden Algebraic Specifications We use hidden algebra as a formal framework for object oriented paradigm. We introduce a labeled transition system for each object specification model, and then define a suitable notion of bisimulation over these models. The labeled transition systems are used to define CTL models of an object specification. Given two hidden algebra models of an object specification, the bisimilar states satisfy the same set of CTL formulas. We build a special CTL model directly from the object specification. Using this CTL model, we can verify the temporal properties using a software tool allowing SMV model checking. A shorter version of the paper was accepted at the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2003). Full document: PS | BibTeX entry TR03-02 (2003) - MpNT: A Multi-Precision Number Theory Package. Number-Theoretic Algorithms (I) MpNT is a multi-precision number theory package developed at the Faculty of Computer Science, "Al.I.Cuza" University of Iasi, Romania. It has been started as a base for cryptographic applications, looking for both efficiency and portability without disregarding code structure and clarity. However, it can be used in any other domain which requires efficient large number computations. The present paper is the first in a series of papers dedicated to the design of the MpNT library. It has two goals. First, it discusses some basic number-theoretic algorithms that have been implemented so far, as well as the structure of the library. The second goal is to have a companion to the courses Algebraic Foundations of Computer Science, Coding Theory and Cryptography, and Security Protocols, where most of the material of this paper has been taught and students were faced with the problem of designing efficient implementations of cryptographic primitives and protocols. From this point of view we have tried to prepare a self-contained paper. No specific background in mathematics or programming languages is assumed, but a certain amount of maturity in these fields is desirable. Due to the detailed exposure, the paper can accompany well any course on algorithm design or computer mathematics. Full document: PS | BibTeX entry TR03-01 (2003) - Concurrent Composition of Objects in Hidden Logic An operator _|_ for concurrent composition of objects specified in hidden logic is proposed and the main properties for this operator are proved. Full document: PS | BibTeX entry TR02-06 (2002) - Transforming Self-Embedded Context-Free Grammars into Regular Expressions Our paper refers to the context-free and regular languages. We point out in an algorithmic manner using system of equations the situations when a context-free grammar generates a regular language: the case of one-letter alphabet and some cases of self-embedded context-free grammars. Moreover, we describe some other sufficient conditions when a self-embedded context-free grammar generates a (non)regular language. The paper proves that the systems of equations with self-embeddedness terms like XaX still have as solution a regular language. In order to enlarge the class of context-free grammars which generates regular languages, the class of one-letter factorizable context-free grammars is introduced. Parts of this technical report have been published as follows: 1. Andrei, St., Cavadini, S.C., Chin, W.N.: A New Algorithm for Regularizing One-Letter Context-Free Grammars. Theoretical Computer Science, Volume 306, Issues 1-3, pp. 113-122 (2003) 2. Andrei, St., Chin, W.N., Cavadini, S.C.: Self-embedded context-free grammars with regular counterparts. Acta Informatica, Volume 40, Number 5, pp. 349-365 (2004) Full document: PS | BibTeX entry TR02-05 (2002) - Coverability Structure Based Analysis Petri nets, vector addition systems, and parallel and communicating grammar systems are three basic theories for modeling and analysing parallel and distributed systems. The aim of this paper is to give an overview on a basic technique of analysis which can be used for all three theories mentioned above. This technique is based on the reduction of an infinite structure to a finite one, called coverability structure. By means of this technique, many decision problems can be discussed in an uniform way. Full document: PS | BibTeX entry TR02-04 (2002) - Decidability and Complexity of Petri Net Problems Petri net theory plays a very important role in modeling and analysing parallel and distributed systems. It provides a simple mathematical structure, and basic properties can be cleanly analysed. The aim of this paper is to give an overview on the basic decision problems in the theory of Petri nets. We discuss both decidability and complexity aspects. We have also a contribution in the area of home markings. We prove that the home marking problem for inhibitor Petri nets is undecidable. Full document: PS | BibTeX entry TR02-03 (2002) - Safety Properties for Petri Nets Modeling and analysing parallel and distributed systems proved to be a real challenge. Many theories have been proposed to accomplish this matter. Among them the Petri net theory plays an important role. This is because a Petri net model is a very simple mathematical structure, but quite expressive. Basic properties of real systems, like safeness or boundedness, liveness, deadlock-freeness, the existence of home markings etc., can be cleanly modeled and analysed by means of Petri nets. The aim of this paper is to give an overview on safeness, liveness, deadlock-freeness and home marking properties of Petri nets. As a contribution, we establish results proving connections between the existence of home markings for confluent and noetherian Petri nets. Full document: PS | BibTeX entry TR02-02 (2002) - The Home Marking Problem and Some Related Concepts
In this paper we study the home marking problem for Petri nets, and some related concepts to it like confluence, noetherianity, and state space inclusion. We show that the home marking problem for inhibitor Petri nets is undecidable. We relate then the existence of home markings to confluence and noetherianity and prove that confluent and noetherian Petri nets have an unique home marking. Finally, we define some versions of the state space inclusion problem related to the home marking and sub-marking problems, and discuss their decidability status. Full document: PS | BibTeX entry TR02-01 (2002) - Subset Based Properties of Partially Ordered Sets
The theory of partially ordered sets (posets, for short) proved to have crucial applications in at least two major fields of computer science: concurrency theory and the semantics of programming languages. In these fields, properties like discreteness, observability, generability, and completeness play an important role. The first three of them have been studied in the literature only for the particular case of finite cardinals and/or at most countable posets. In this paper we generalize the properties of discreteness, observability, and generability by allowing arbitrarily large cardinals. The results we obtain extend in a proper way many of the results obtained until now regarding these properties. Concerning completeness properties, we adopt a general definition using subset systems, and then investigate the relationships between various concepts of completeness. Full document: PS | BibTeX entry TR01-01 (2001) - On Concurrency-Degrees for Petri Nets Petri nets are a mathematical model used for the specification and the analysis of parallel/distributed systems. It is very important to introduce a measure of concurrency for parallel/distributed systems, so that we can speak about what is the meaning of the fact that in the system S1 the concurrency is greater than in the system S2. The notion of concurrency-degrees for Petri nets has been formulated in [TJD93], and for jumping Petri nets in [JuV00]. But these definitions have a drawback: they take into consideration only distinct transitions which can fire simultaneously; thus, they ignore the auto-concurrency, i.e. the case of a transition fireable simultaneously with itself at a marking. In this paper we give a more general definition of concurrency-degree for Petri nets and for jumping Petri nets, which takes into consideration also the auto-concurrency, for replacing the old definitions which ignore the auto-concurrency. Moreover, we show how we can compute these more general concurrency-degrees. Full document: PS | BibTeX entry TR00-03 (2000) - Structuri abstracte pentru interactiune TR00-02 (2000) - Inductie si recursie pe domeniile inductiv definite TR00-01 (2000) - Concurent Composition, Refinement, and Fairness in CafeOBJ
The paper exhibit the power of the Cafeobj system to handle concurrency, synchronization, nondeterminism, and communication in specification of complex systems. A simple and efficient method to handle the fairness assumption in proofs is shown. Full document: PS | BibTeX entry TR99-03 (1999) - WDS'99 The Scientific Programme and Communications TR99-02 (1999) - Eurolan'99 (4-th) Eurolan Summer School on Human Language Technology TR99-01 (1999) - On the Object Aggregation in CafeOBJ: Three Case Studies
Aggregation is the ``part-whole'' relationship in which objects representing the components are associated with a composite object representing the entire ensemble. In this paper we propose a methodology for specifying composite objects in algebraic specification languages like CafeOBJ. We study three kinds of aggregation: aggregation of concurrent objects, aggregation of synchronized objects, and aggregation of communicating objects. We show that the methodology is safe in the sense that if we refine a component then the result composite object refines the initial composite object. Full document: PS | BibTeX entry TR98-04 (1998) - Boundary Control Approximation of a 1-dimensional Hyperbolic Equation TR98-03 (1998) - On the Axiomatization of Categories of Symmetries
In this paper we investigate the possibilities to obtain complete axiomatizations for categories of symmetries. The key point consists in associating a rewrite theory $\calR(\S,E)$ with the equational specification by turning the equations into rewrite rules. The elegant construction of the free $\calR$-grupoid given in \cite{concrew} provides already an axiomatization of the free $(\S,E)$-system (the non-coherent category of symmetries). The problem of finding axioms which expresses the commutativity of the diagrams still remains. We show that if equations $E$, viewed as rewrite rules, form a convergent (confluent and terminating) rewriting system then these axioms are obtained by computing all critical pairs. Each confluent rewriting generated by a critical pair produce an equation. The set of all equations obtained in this way forms a specification of the commutative diagrams. The method can be generalized to the case when $E$ is convergent modulo a theory $T$. Full document: PS | BibTeX entry TR98-02 (1998) - Aproximarea problemelor de control optimal guvernate de ecuatii neliniare infinit dimensionale (Ph.D. Dissertation) TR98-01 (1998) - Logici neclasice si programare logica (Ph.D. Dissertation) |