Technical Reports
-
TR21-01 (2021) – Improving Lower Bounds for Equitable Chromatic Number
Emanuel Florentin Olariu, Cristian Frasinaru
In many practical applications the underlying graph must be as equitable colored as possible. A coloring is called equitable if the number of vertices colored with each color differs by at most one, and the least number of colors for which a graph has such a coloring is called its equitable chromatic number.
We introduce a new integer linear programming approach for studying the equitable coloring number of a graph and show how to use it for improving lower bounds for this number. The two stage method is based on finding or upper bounding the maximum cardinality of an equitable color class in a valid equitable coloring and, then, sequentially improving the lower bound for the equitable coloring number.
The computational experiments were carried out on DIMACS graphs and other graphs from the literature.
-
TR20-03 (2020) – A Branch and Bound Algorithm for Coalition Structure Generation over Graphs
Emanuel Florentin Olariu, Cristian Frasinaru, Albert Abel Policiuc
We give a column generation based branch and bound algorithm for coalition structure generation over graphs problem using valuation functions for which this problem is proven to be NP-complete. For a given graph G = (V;E) and a valuation function w : 2^V -> R, the problem is to find the most valuable coalition structure (or partition) of V . We consider two cases: first when the value of a coalition is the sum of the weights of its edges which can be positive or negative, second when the value of a coalition takes account of both inter- and intra-coalitional disagreements and agreements, respectively. For both valuations we give experimental results which cover for the first time sets of more than forty agents.
For another valuation function (coordination) we give only the theoretical considerations in the appendix.
-
TR20-02 (2020) – Multiple-Depot Vehicle Scheduling Problem Heuristics
Emanuel Florentin Olariu, Cristian Frasinaru
The Multiple-Depot Vehicle Scheduling Problem (MDVSP) is very important in the planning process of transport systems. It consists in assigning a set of trips to a set of vehicles in order to minimize a certain total cost. We introduce three fast and reliable heuristics for MDVSP based on a classical integer linear programming formulation and on graph theoretic methods of fixing the infeasible subtours gathered from an integer solution. Extensive experimentations using a large set of benchmark instances show that our heuristics are faster and give good or even better results compared with other existing heuristics.
-
TR20-01 (2020) – Exploiting Social Networks. Technological Trends (Habilitation Thesis)
Adrian Iftene
The habilitation thesis presents two main directions:
- Exploiting data from social networks (Twitter, Facebook, Flickr, etc.) – creating resources for text and image processing (classification, retrieval, credibility, diversification, etc.);
- Creating applications with new technologies : augmented reality (eLearning, games, smart museums, gastronomy, etc.), virtual reality (eLearning and games), speech processing with Amazon Alexa (eLearning, entertainment, IoT, etc.).
The work was validated with good results in evaluation campaigns like CLEF (Question Answering, Image CLEF, LifeCLEF, etc.), SemEval (Sentiment and Emotion in text, Anorexia, etc.).
-
TR19-01 (2019) – A Note on Sequences of Lattices
Emanuel Florentin Olariu
We investigate the relation between the convergence of a sequence of lattices and the set-theoretic convergence of their corresponding Voronoi cells sequence. We prove that if a sequence of full rank lattices converges to a full rank lattice, then the closures of the limit infimum and limit supremum of the Voronoi cells converges to the corresponding Voronoi cell. It remains an open question if the converse is also true.
-
TR16-01 (2016) – RMT: Proving Reachability Properties in Constrained Term Rewriting Systems Modulo Theories
Stefan Ciobaca, Dorel Lucanu
We introduce the {\tt RMT} tool, which takes as input a constrained term rewriting system $\R$ and proves reachability properties of the form $\forall \tilde{x}.(c_1(\tilde{x}) \rightarrow \exists \tilde{y}.(c_2(\tilde{x}, \tilde{y}) \land t_1(\tilde{x}) \goesall_\R^* t_2(\tilde{x}, \tilde{y})))$, where $c_1, c_2$ are constraints over the variables $\tilde{x}$ and respectively $\tilde{x} \cup \tilde{y}$ and $t_1, t_2$ are terms over the variables $\tilde{x}$ and respectively $\tilde{x} \cup \tilde{y}$. By the relation $\goesall_\R^*$, we mean that $t_2(\tilde{x}, \tilde{y})$ is reachable across all paths in $\R$ starting in $t_1(\tilde{x})$. The reachability guarantee is sound for terminating paths starting in instances of $t_1(\tilde{x})$ and it was initially motivated by proving partial correctness of programs. The constrained term rewriting system is allowed to contain both interpreted and uninterpreted function symbols. The interpreted symbols are part of a theory that is a parameter to our tool and all rewriting steps are defined \emph{modulo} this theory. In practice, the interpreted symbols are handled by relying on an SMT solver.
-
TR15-02 (2015) – Maximum cardinality popular matchings in the stable marriage problem
Emanuel Olariu, Cristian Frasinaru
Popular matching and was extensively studied in recent years as an alternative to stable matchings.Both type of matchings are defined in the framework of Stable Marriage (SM) problem: in a givenbipartite graph G = (A;B;E) each vertex u has a strict order of preference on its neighborhood. Amatching M is popular, if for every matching M ‘ of G, the number of vertices that prefer M ‘ to M isat most the number of vertices which prefer M to M ‘. In this paper we prove that every maximumcardinality popular matching saturates the same set of vertices. This property is similar to that ofstable matchings: any such matching saturates the same set of vertices.
-
TR15-01 (2015) – Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version)
Andrei Arusoaie, Dorel Lucanu, David Nowak, Vlad Rusu
Reachability Logic is a recently introduced formalism, whichis currently used for defining the operational semantics of programminglanguages and for stating properties about program executions. In thispaper we show how Reachability Logic can be adapted for stating propertiesof transition systems described by Rewriting-Logic specifications.We propose an automatic procedure for verifying Rewriting-Logic specificationsagainst Reachability-Logic properties. We prove the soundnessof the procedure and illustrate it by verifying a communication protocolspecified in Maude.
-
TR14-01 (2014) – A Language-Independent Proof System for Mutual Program Equivalence (revisited)
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
Two programs are mutually equivalent if they both diverge or they end up in similar states. Mutual equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: if it terminates then it establishes the mutual equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence.
-
TR13-03 (2013) – A Language-Independent Proof System for Mutual Program Equivalence
Stefan Ciobaca, Dorel Lucanu, Vlad Rusu, Grigore Rosu
Two programs or fragments of program are mutually equivalent iff either theyboth diverge or they end up in similar states.Mutual equivalence is desirable in many contexts, ranging from capturingprogram equivalence or correctness of program transformations withinthe same language, to capturing correctness of compilersfrom one language to another.This paper introduces a language-independent proof system for mutualequivalence.The proof system is parametric in the operational semantics of the twolanguages and in a state similarity relation.
-
TR13-02 (2013) – A simple push-relabel algorithm for sub-modular flows
Cristian Frasinaru, Emanuel Olariu
In this paper we present a combinatorial push-relabel algorithm for sub-modular flows. Ourprocedure, using a lowest level rule combined with a bfs-like traversal, needs no lexicographic orderof the elements, and gives a time complexity of Ο(n5).
-
TR13-01 (2013) – A New Strategy for Push-Relabel Algorithm Framework for Matroid Optimization
Emanuel Olariu
In this paper we present a combinatorial push-relabel algorithm based on lowest level/bfs traversal for matroid optimization. In contrast with other known algorithms our procedure uses lowest level rule and needs no lexicographic order of the elements. Combined with a reduction of the number of active basis our strategy gives a time complexity of Ο(n6).
-
TR12-03(version 2) (2012) – CinK – an exercise on how to think in K
Dorel Lucanu, Traian Florin Serbanuta
-
TR12-03 (2012) – CinK – an exercise on how to think in K
Dorel Lucanu, Traian Florin Serbanuta
CinK is a kernel of the C++ language we used to experiment with K. The language is used an example for teachingclasses and is refered in several research papers.
In this report we briefly present the K definition of CinK. The most part of the text is automatically generatedwith the K tool, therefore there are some differences between the source code and the pdf version. For instance,the terminal syntax declarations are enclosed into quotes but in the pdf version these are not displayed. In thepdf version, for ease of reading reasons, there are used different fonts in order to distinguish between differentsyntactic categories.
The report is not intended to be an introduction to K. We assume the reader is already familiar with theK Framework and the K tool and here we try to share our experience in defining a languages with some specificfeatures, as C++ is. Such features includes a clear distinction between l-values and r-values, declaration of aliases,and various parameters passing mechanisms. We also extend the definition with a small property language,including LTL formulas, and we show how the K tool is used together with Maude system for analazing CinKprograms.
The K definition of CinK is continuously evolving, so this report presents the status of this definition at thepublication date.
-
TR12-02 (2012) – Importance Sampling using Rényi divergence
Emanuel Olariu
We present an alternative approach to the problem of estimatingprobabilities of rare events and for optimization problems using the classof Rényi divergences of order α > 1. The general procedure wedescribe does not involve any specific family of distributions, the onlyrestriction is that the search space consists of product form probabilitydensity functions. We discuss an algorithm for estimation of probability ofrare events and a version for continuous optimization. The results ofnumerical experimentation with these algorithms carried in the last sectionsupport their performances.
-
TR12-01 (2012) – Importance Resampling with MRAS algorithm for Bermudan option pricing
Emanuel Olariu
In this paper we investigate a MRAS type algorithm for pricing Bermudanoption. We use three different model for the price dynamics: geometricBrownian, Merton jump-diffusion and a relative new one, namely, the doubleasymmetric exponentially jump-diffusion model. Although MRAS procedureincludes a form of importance sampling we modify the original procedure inorder 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 MRASand very reliable offering small confidence intervals.
-
TR11-01 (2011) – Learning to unlearn in lattices of concepts: A case study in Fluid Construction Grammars
Liviu Ciortuz, Vlad Saveluc
This report outlines a couple of lattice-based (un)learningstrategies proposed in a recent development ofunification-based grammars, namely the Fluid ConstructionGrammar (FCG) setup.
These (un)learning strategies are inspired by two linguisticphenomena occurring in a dialect spoken in the Banatarea of Romania. Children from that region – whereinfluences produced over centuries by Serbian, a Slaviclanguage, are obvious – learn in school the modernRomanian language, which is a Romance language.
This particular setup offers us the possibility to modelin FCG a two-step learning process: the first step isthat of learning a (perfective) verbal aspect similar tothe one already presented by Kateryna Gerasymova inher MSc thesis, while the second one is concerned withun-learning (or, learning another linguistic “construction”over) this verbal aspect. Thus, the interesting issue here ishow learning could continue beyond learning the verbalaspects. We will first give linguistic facts, after which wewill outline the way in which FCG could model such alinguistic process.
From the computational point of view, we show that theheuristics used in this grammar repairing process can beautomatically derived since the meanings associated towords and phrases are organized in a lattice of featurestructures, according to the underlying constraint logics.
We will later discuss the case of another verbal markerin the dialect spoken in Banat. It will lead us to sketch acomposite, quite elaborated (un)learning strategy.
-
TR10-05 (2010) – Automating Coinduction with Case Analysis
Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu
Coinduction is a major technique employed to prove behavioralproperties of systems, such as behavioral equivalence. Its automationis highly desirable, despite the fact that most behavioral problemsare $\Pi_2^0$-complete. Circular coinduction, which is at the core of the CIRCprover, automates coinduction by systematically deriving new goals andproving existing ones until, hopefully, all goals are proved. Motivatedby practical examples, circular coinduction and CIRC have been recentlyextended with several features, such as special contexts, generalizationand simplification. Unfortunately, none of these extensions eliminatesthe need for case analysis and, consequently, there are still many naturalbehavioral properties that CIRC cannot prove automatically. Thispaper presents an extension of circular coinduction with case analysisconstructs and reasoning, as well as its implementation in CIRC. To uniformlyprove the soundness of this extension, as well as of past and futureextensions of circular coinduction and CIRC, this paper also proposes ageneral correct-extension technique based on equational interpolants.
-
TR10-04 (2010) – Languages attached to Parikh Matrices
Radu-Florian Atanasiu
This report presents an approach of formal languages based on Parikh matrices. We will display severalpoints of characterizing various aspects of languages using Parikh matrices and the Parikh matrixmapping. The results included in this report are mainly obtained in [Atanasiu, R., 2010].
-
TR10-03 (2010) – Applications of Parikh Matrices in Coding Theory
Radu-Florian Atanasiu
In this report we will describe a possible application of Parikh matrices and amiability in the field ofinformation security. The results presented were developed in [Atanasiu, A. & Atanasiu, R., 2008].
-
TR10-02 (2010) – FCGlight: Making the bridge between Fluid Construction Grammars and main-stream unification grammars by using feature constraint logics
Liviu Ciortuz
Fluid Construction Grammars (FCGs) are a flavour of Construction Grammars,which themselves are unification-based grammars. Its syntax is (only) up tocertain extent similar to other unification-based grammars. However, it lacks adeclarative semantics, while its procedural semantics is truly particular, comparedto other unification-based grammar formalisms.
Here we propose the re-definition of a subset of the FCG formalism (henceforthcalled FCGlight) within the framework of (order-sorted) feature constraintlogics (OSF-logic) that would assign FCG a rigorous (both declarative a and procedural)semantics, which is suitable for both parsing, generation and grammarlearning.
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 paradigmfor 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 withthe linguistic background knowledge when devising the grammar repair strategiesand a clear way to compare different grammars that could be learned by anagent at each step during the grammar evolution process.
In return, inspired by the FCG approach to grammar learning, we are able todefine new ways for learning grammars in other unification-based formalisms. Inparticular, ILP-like learning of HPSGs can be substantially improved by usingideas borrowed from FCG:
– instead of using a given “golden” test suite (against which the learning isperformed), this test suite is dynamically produced during the language game(played by two agents);
– the grammar learning process will be “grounded”, something which was notconsidered before;
– we will learn also new rules (instead of modifying the given ones, as currentlydone in ilpLIGHT)
– learning new rules by generalising upon already learned rules, will also be asignificant step forward.
-
TR10-01 (2010) – Yet Another SVM for MiRNA Recognition: yasMiR
Daniel Pasaila, Irina Mohorianu, Andrei Sucila, Stefan Pantiru, Liviu Ciortuz
We designed a new SVM for microRNA identification,whose novelty is two-folded: firstly many of its features incorporatethe base-pairing probabilities provided by McCaskill’s algorithm, and secondly the classification performanceis improved by using a certain similarity (“profile”-based) measure between the training and test microRNAsand a set of carefully chosen (“pivot”) RNA sequences.Comparisons with some of the best existing SVMs for microRNAidentification prove that our SVM obtains trulycompetitive results.
-
TR09-04 (2009) – Ontology-Based Modeling and Recommendation Techniques for Adaptive Hypermedia Systems
Mihaela Brut
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania,for the degree of Doctor of Philosophy in Computer Science.
-
TR09-03 (2009) – Time Constraints in Workflow Net Theory
Geanina Ionela Macovei
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania,for the degree of Doctor of Philosophy in Computer Science.
-
TR09-02 (2009) – Textual Entailment
Adrian Iftene
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania,for the degree of Doctor of Philosophy in Computer Science.
-
TR09-01 (2009) – Securing the Media Stream Inside VoIP SIP Based Sessions
Emanuel Onica
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).
-
TR08-03 (2008) – Learning to Unroll Loops Optimally
Stefan Ciobaca, Liviu Ciortuz
Every few months new types of hardware are released. Compiler writers facethe challenging task of keeping the compiler optimizations up-to-date with the latestin hardware technology. In this paper we apply machine learning techniquesto predict the best unroll factors for loops, using GCC and the x86 architecture forour experiments. We show that, depending on the machine learning tools used, weget similar or slightly better performance than the native GCC loop optimizer. Ourresult shows that machine learning techniques can be used to automatically trainthe heuristic that computes the unroll factor for loops, saving time for compilermanufacturers and providing better performance in the case of scientific computations.
-
TR08-02 (2008) – A Rewrite Stack Machine for ROC!
G. Caltais, E.-I. Goriac, D. Lucanu, G. Grigoras
ROC! is a deterministic rewrite strategy language which includes the rewriterules as basic operators, and the deterministic choice and the repetitionas 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 thatR’-rewriting is equivalent (sound and complete) with R-rewriting constrained byROC!. Since R’ uses a stack, it is called a rewrite stack machine.
-
TR08-01 (2008) – Support Vector Machines for MicroRNA Identification
Liviu Ciortuz
This technical report provides an overview on the support vector machines that have been designed during the recent years for theidentification of microRNA sequences. Our aim is to arrive in the endto identify potential ways in which the quality of such machine learning methods could be [...]
-
TR07-02 (2007) – Secrecy for Security Protocols
Catalin Birjoveanu
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania,for the degree of Doctor of Philosophy in Computer Science.
-
TR07-01 (2007) – Secret Sharing Schemes with Applications in Security Protocols
Sorin Iftene
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania,for the degree of Doctor of Philosophy in Computer Science.
-
TR06-01 (2006) – Strategies and Tactics in Operational Semantics
Oana Andrei, Gabriel Ciobanu, Dorel Lucanu
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 astrategy 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 [...]
-
TR05-07 (2005) – Embedding mobile ambients into the pi-calculus
Gabriel Ciobanu, Vladimir Zakharov
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 λ-calculus, and the π-calculus. In this paper we demonstrate that we have a closer relationship between mobile ambients and the π-calculus. We present an embedding of pure mobile ambients into a fragment of the π-calculus [...]
-
TR05-06 (2005) – A Comparative Study on Feature Selection Algorithms in Data Mining
Luminita Mihaela Moruz, Liviu Ciortuz
The field of feature selection in data mining has experienced a great development in the past few years. Unfortunately, there are few worksthat show a comparative analysis of feature selection algorithms introduced until now. [...]
-
TR05-05 (2005) – Threshold RSA Based on the General Chinese Remainder Theorem
Sorin Iftene
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. [...]
-
TR05-04 (2005) – Walking the Royal Road with Integrated-Adaptive Genetic Algorithms
Ovidiu Gheorghies, Henri Luchian, Adriana Gheorghies
The aim of this paper is to show that exploiting knowledge extracted from the optimization process is important for thesuccess 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. [...]
-
TR05-03 (2005) – An Ordering-Based Genetic Approach to Graph Coloring
Cornelius Croitoru, Ovidiu Gheorghies, Adriana Gheorghies
We introduce a new evolutionary formulation of the graphcoloring problem, based on the interplay between orderings and coloringsof 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 [...]
-
TR05-02 (2005) – Decidability and Complexity Results for Security Protocols
F. L. Tiplea, C. Enea, C. V. Birjoveanu
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. [...]
-
TR05-01 (2005) – Web Ontology Verification and Analysis in the Z Framework
D. Lucanu, Y. F. Li, J. S. Dong
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 [...]
-
TR04-04 (2004) – Proprietati structurale ale retelelor Petri
Cristian Vidrascu
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science.
-
TR04-03 (2004) – Modular Analysis of Petri Net Models
Aurora Tiplea
Thesis submitted to the “Alexandru Ioan Cuza” University of Iasi, Romania, for the degree of Doctor of Philosophy in Computer Science.
-
TR04-02 (2004) – Invariants and Verification of Properties for Jumping Petri Nets
Cristian Vidrascu
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.
-
TR04-01 (2004) – ADF – Abstract Framework for Developing Mobile Agents
O. Nichifor, S. Buraga
In this technical report, the authors propose an abstract framework, called ADF (Agent Developing Framework), to be used indesigning 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. [...]
-
TR03-06 (2003) – Structuri de accesibilitate reduse pentru retele Petri de nivel inalt
Cristian Vidrascu
Aceasta lucrare prezinta o sinteza asupra structurilor de accesibilitate si de acoperire,precum si a aplicatiilor acestora, pentru retele Petri de nivel inalt.
-
TR03-05 (2003) – Specification and Verification of Synchronized Concurrent Objects
G. Ciobanu, D. Lucanu
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 hidden CCS, 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. [...]
-
TR03-04 (2003) – Incremental Counting Satisfiability for Real-Time Systems
S. Andrei, W.-N. Chin
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. [...]
-
TR03-03 (2003) – Behavioral Bisimulation and CTL Models for Hidden Algebraic Specifications
D. Lucanu, G. Ciobanu
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 anobject specification. Given two hidden algebra models of an object specification, the bisimilar states satisfy the same set of CTL formulas. [...]
-
TR03-02 (2003) – MpNT: A Multi-Precision Number Theory Package. Number-Theoretic Algorithms (I)
F.L. Tiplea, S. Iftene, C. Hritcu, I. Goriac, R.M. Gordan, E. Erbiceanu
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. [...]
-
TR03-01 (2003) – Concurrent Composition of Objects in Hidden Logic
Dorel Lucanu
An operator _|_ for concurrent composition of objects specified in hidden logic is proposed and the main properties for this operator are proved.
-
TR02-06 (2002) – Transforming Self-Embedded Context-Free Grammars into Regular Expressions
St.Andrei, S.Cavadini, W-N. Chin
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. [...]
-
TR02-05 (2002) – Coverability Structure Based Analysis
Roxana Melinte
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. [...]
-
TR02-04 (2002) – Decidability and Complexity of Petri Net Problems
Olivia Oanea
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. [...]
-
TR02-03 (2002) – Safety Properties for Petri Nets
Ioana Olga
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 theoryplays 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 safenessor boundedness, liveness, deadlock-freeness [...]
-
TR02-02 (2002) – The Home Marking Problem and Some Related Concepts
R. Melinte, O. Oanea, I. Olga, F.L. Tiplea
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 [...]
-
TR02-01 (2002) – Subset Based Properties of Partially Ordered Sets
F.L. Tiplea, S. Iftene, B. Ciurariu, C. Apachite
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. [...]
-
TR01-01 (2001) – On Concurrency-Degrees for Petri Nets
Cristian Vidrascu, Toader Jucan
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]. [...]
-
TR00-03 (2000) – Structuri abstracte pentru interactiune
Gabriel Ciobanu, Florentin Olariu
-
TR00-02 (2000) – Inductie si recursie pe domeniile inductiv definite
Ferucio Laurentiu Tiplea
-
TR00-01 (2000) – Concurent Composition, Refinement, and Fairness in CafeOBJ
Dorel Lucanu, Shusaku Iida, Razvan Diaconescu
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.
-
TR99-03 (1999) – WDS’99 The Scientific Programme and Communications
D. Lucanu, Gh. Stefanescu (editors)
-
TR99-02 (1999) – Eurolan’99 (4-th) Eurolan Summer School on Human Language Technology
D. Cristea et. al. (eds.)
-
TR99-01 (1999) – On the Object Aggregation in CafeOBJ: Three Case Studies
Dorel Lucanu
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. [...]
-
TR98-04 (1998) – Boundary Control Approximation of a 1-dimensional Hyperbolic Equation
Anca Ignat
-
TR98-03 (1998) – On the Axiomatization of Categories of Symmetries
Dorel Lucanu
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). [...]
-
TR98-02 (1998) – Aproximarea problemelor de control optimal guvernate de ecuatii neliniare infinit dimensionale (Ph.D. Dissertation)
Anca Ignat
-
TR98-01 (1998) – Logici neclasice si programare logica (Ph.D. Dissertation)
Cristian Papp