Technical Reports

TR2101 (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.

TR2003 (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 NPcomplete. 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 intracoalitional 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.

TR2002 (2020) – MultipleDepot Vehicle Scheduling Problem Heuristics
Emanuel Florentin Olariu, Cristian Frasinaru
The MultipleDepot 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.

TR2001 (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.).

TR1901 (2019) – A Note on Sequences of Lattices
Emanuel Florentin Olariu
We investigate the relation between the convergence of a sequence of lattices and the settheoretic 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.

TR1601 (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.

TR1502 (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.

TR1501 (2015) – Verifying ReachabilityLogic Properties on RewritingLogic 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 RewritingLogic specifications.We propose an automatic procedure for verifying RewritingLogic specificationsagainst ReachabilityLogic properties. We prove the soundnessof the procedure and illustrate it by verifying a communication protocolspecified in Maude.

TR1401 (2014) – A LanguageIndependent 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 languageindependent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a statesimilarity 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.

TR1303 (2013) – A LanguageIndependent 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 languageindependent proof system for mutualequivalence.The proof system is parametric in the operational semantics of the twolanguages and in a state similarity relation.

TR1302 (2013) – A simple pushrelabel algorithm for submodular flows
Cristian Frasinaru, Emanuel Olariu
In this paper we present a combinatorial pushrelabel algorithm for submodular flows. Ourprocedure, using a lowest level rule combined with a bfslike traversal, needs no lexicographic orderof the elements, and gives a time complexity of Ο(n^{5}).

TR1301 (2013) – A New Strategy for PushRelabel Algorithm Framework for Matroid Optimization
Emanuel Olariu
In this paper we present a combinatorial pushrelabel 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 Ο(n^{6}).

TR1203(version 2) (2012) – CinK – an exercise on how to think in K
Dorel Lucanu, Traian Florin Serbanuta

TR1203 (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 lvalues and rvalues, 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.

TR1202 (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.

TR1201 (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 jumpdiffusion and a relative new one, namely, the doubleasymmetric exponentially jumpdiffusion 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.

TR1101 (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 latticebased (un)learningstrategies proposed in a recent development ofunificationbased 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 twostep 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 withunlearning (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.

TR1005 (2010) – Automating Coinduction with Case Analysis
EugenIoan 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 correctextension technique based on equational interpolants.

TR1004 (2010) – Languages attached to Parikh Matrices
RaduFlorian 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].

TR1003 (2010) – Applications of Parikh Matrices in Coding Theory
RaduFlorian 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].

TR1002 (2010) – FCGlight: Making the bridge between Fluid Construction Grammars and mainstream unification grammars by using feature constraint logics
Liviu Ciortuz
Fluid Construction Grammars (FCGs) are a flavour of Construction Grammars,which themselves are unificationbased grammars. Its syntax is (only) up tocertain extent similar to other unificationbased grammars. However, it lacks adeclarative semantics, while its procedural semantics is truly particular, comparedto other unificationbased grammar formalisms.
Here we propose the redefinition of a subset of the FCG formalism (henceforthcalled FCGlight) within the framework of (ordersorted) feature constraintlogics (OSFlogic) 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 unificationbased 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 unificationbased formalisms. Inparticular, ILPlike 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.

TR1001 (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 twofolded: firstly many of its features incorporatethe basepairing 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.

TR0904 (2009) – OntologyBased 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.

TR0903 (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.

TR0902 (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.

TR0901 (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).

TR0803 (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 uptodate 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.

TR0802 (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 highlevel 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 Rrewriting constrained byROC!. Since R’ uses a stack, it is called a rewrite stack machine.

TR0801 (2008) – Support Vector Machines for MicroRNA Identification
Liviu Ciortuz
This technical report provides an overview on the supportvector 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 learningmethods could be further improved, knowing that the rate of falsepositves they produce is still too high.

TR0702 (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.

TR0701 (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.

TR0601 (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 evaluationstrategies (as eager or lazy evaluations). We use these strategies to define semantics of a systemstarting 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 isthe goal” of a computation, the tactics are at a lower level and tell “how it is possible to reachthe goal”.
We use rewriting systems as a general model of computing. In this framework we give anoperational semantics of the strategic transitions in terms of tactical rewritings. The approachis inspired by a new model of computation given by membrane systems. We define the strategysemantics for membrane systems involving the maximal parallel rewriting and priorities. Weshow that strategies are not powerful enough to define alone the semantics of membrane systemsinvolving promoters. This is possible when we encode the state of the membrane in a richerstructure.

TR0507 (2005) – Embedding mobile ambients into the picalculus
Gabriel Ciobanu, Vladimir Zakharov
The mobile ambient paradigm of mobile computations is very expressive andallows various embeddings into it of other models of computations such asTuring machine, the lambdacalculus, and the picalculus. In this paper wedemonstrate that we have a closer relationship between mobile ambients andthe picalculus. We present an embedding of pure mobile ambients into afragment of the picalculus, namely the localized sumfree synchronousmonadic picalculus with matching and mismatching. The embedding isachieved by associating a pair of localized piterms Structure_A and Rulerto every mobile ambient A. Structure_A simulates the spatial structure ofA by means of communication channels. Ruler is a universal piprocessintended to simulate the operational semantics of the mobile ambients.This embedding of pure mobile ambients into a subset of the picalculusopens new ways to the analysis of ambients by means of techniques used inthe picalculus.

TR0506 (2005) – A Comparative Study on Feature Selection Algorithms in Data Mining
Luminita Mihaela Moruz, Liviu Ciortuz
The field of feature selection in data mining hasexperienced a greatdevelopment in the past few years. Unfortunately,there are few worksthat show a comparative analysis of feature selectionalgorithmsintroduced until now.
In this technical report we analyze the effect thatfeature selectionhas on the performance of five learning algorithms. Weuse nine of themost known feature selection algorithms. We conductour study on twoclassification problems, Dermatology and Zoo, whosedatasets areprovided in the UCI (University of California atIrvine) repository.
We realize a comparative study on the effects that thechosen featureselection algorithms have on the performance and therunning time of thelearning algorithms used in solving the two problems.
On these problems, the feature selection algorithmsprovide an accuracywhich is 1.09% and respectively 1.98% higher than theaccuracy obtainedby learning algorithms alone. Additionally, thereduction of running timeespecially for time consuming learning algorithms likeSVMO is highlysignificant, 59% and respectively 91%.

TR0505 (2005) – Threshold RSA Based on the General Chinese Remainder Theorem
Sorin Iftene
In threshold (or grouporiented) 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 combiningmultiplicative secret sharing schemes with homomorphic cryptographic operations. In this paper we focus on threshold RSA decryption and thresholdRSA digital signature generation.More exactly, we combine the threshold secret sharing schemes based on the Chinese remainder theoremwith the RSA cryptosystem, as an alternative to the classicalsolutions based on the Shamir’s threshold secret sharing scheme.

TR0504 (2005) – Walking the Royal Road with IntegratedAdaptive Genetic Algorithms
Ovidiu Gheorghies, Henri Luchian, Adriana Gheorghies
The aim of this paper is to show that exploiting knowledgeextracted from the optimization process is important for thesuccess of an evolutionary solver. In the context of NK fitnesslandscapes, we identify two causes for the difficulty ofan optimization problem: the intrinsic combinatorial difficultyand the randomsearch hybridization. We apply theseconcepts for the royal road fitness landscape. Experimentalresults indicate that IntegratedAdaptive Genetic Algorithms(IAGA) are particularly suited for tackling randomsearchhybridization. A learnasyougo system aimed at afinegrained adaptation of operators behavior increases thesolving power and convergence speed of IAGA. We concludethat the royal road problem is actually being “royal”for the traditional GA, but for a class of adaptive geneticalgorithms.

TR0503 (2005) – An OrderingBased 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 inthe solution space and provides opportunities for combining evolutionaryand other search techniques. Our formulation is very simple comparedto previous approaches which use the relationship between a graph’schromatic number and its acyclic orientations. We have experimentedon graphs from the DIMACS Computational Challenge. The results provideevidence that the ordering approach can be used to obtain accuratecolorings. We also give a general property which accounts for the computationaldifficulty of all approaches that attempt to iteratively reduce the number ofcolors in a coloring.

TR0502 (2005) – Decidability and Complexity Results for Security Protocols
F. L. Tiplea, C. Enea, C. V. Birjoveanu
Security protocols are prescribed sequences of interactions between entitiesdesigned to provide various security services across distributed systems. Securityprotocols are often wrong due to the extremely subtle properties they are supposedto ensure. Deciding whether or not a security protocol assures secrecy is one ofthe main challenge in this area.In this paper we survey the most important decidability and complexity resultsregarding the secrecy problem for various classes of security protocols, such asbounded protocols, finitesessions protocols, normal protocols, and tagged protocols.All the results are developed under the same formalism. Several flawed statementsclaimed in the literature are corrected. Simplified proofs and reductions, aswell as slight extensions of some known results, are also provided.

TR0501 (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 importantaspect in the development of reliable Semantic Web systems.Software specification and verification tools can be used tocomplement the Knowledge Representation tools in reasoning aboutSemantic Web. The key for applying software verification toolsto Semantic Web is to develop the sound transformation techniquesfrom Web ontology to software specification models so that theassociated verification tools can be applied to check the transformedspecification models. Our previous work has demonstrated a practicalapproach to translating Web ontologies to Z specification models.However, from a sound engineering point of view, the translationis lacking the theoretical work that can formally relate the respectiveunderlying logical systems in semantic web and Z.In this paper, we show that the logics underlying OWL, SWRL, and SWRL FOLcan be represented as institutions, we investigate the properties of theseinstitutions, and we show that the institutioncomorphism provides a formal semantic foundation for encoding web ontologiesspecifications in Z.

TR0404 (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.

TR0403 (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.

TR0402 (2004) – Invariants and Verification of Properties for Jumping Petri Nets
Cristian Vidrascu
This paper presents the notions of place and transition invariantsfor jumping Petri nets, and the results concerning invariantsextended to them from classical Petri nets.Moreover, it presents some examples of systems modelled byjumping Petri nets and the verification of their propertiesusing the invariant method.

TR0401 (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 amultiagent architecture. We also investigate the possibility ofdeveloping, in a generic manner, different components to be integratedinto agent applications. The ADF framework consists of a hierarchy ofclasses (structured as a Java package) and a visual developing tool. Theproposed API offers the core functionalities of an agentoriented system(e.g., agents, hosts, name service, migration, and messaging).

TR0306 (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.

TR0305 (2003) – Specification and Verification of Synchronized Concurrent Objects
G. Ciobanu, D. Lucanu
Hidden algebra is used to specify object systems, and CCS is used todescribe synchronous concurrent systems. We introduce a newspecification formalism which we call hiddenCCS, formedby extending the object specification with synchronizationelements related to the invocation of complementary methods in differentobject components, and using a CCS coordinating module able to describethe interaction patterns of method invocations. Various results refer tostrong bisimulation over the hiddenCCS configurations. We show that weakbisimulation allows for specification development by stepwise refinement.We investigate how the existing tools CWB, BOBJ, Maude can be integratedto describe and verify useful properties of the synchronized concurrentobjects. The hiddenCCS specifications can be described in the rewritinglogic of Maude. Finally we present the first steps towards a newCTL verification tool for hiddenCCS.
A concise and revised version of the paper was accepted at the FourthInternational Conference on Integrated Formal Methods(IFM2004).

TR0304 (2003) – Incremental Counting Satisfiability for RealTime Systems
S. Andrei, W.N. Chin
Counting the number of truth assignments in a propositional formula has anumber of applications, including the verification of timing constraintsforrealtime specification. This number can tell us how “far away” is agivenspecification from satisfying its safety assertion. However,specificationsand safety assertions are often modified in an incremental fashion, whereproblematic bugs are fixed one at a time. To mirror such changes, wepropose an incremental algorithm for counting satisfiability. Ourproposedincremental algorithm is optimal as no unnecessary nodes are createdduring each incremental counting. To illustrate this application, we showhow incremental satisfiability counting can be applied to a wellknownrailroad crossing example, when its specification is being modified.
A concise and revised version of the paper was accepted at the10th IEEE RealTime and Embedded Technology and Applications Symposium(RTAS 2004).

TR0303 (2003) – Behavioral Bisimulation and CTL Models for Hidden Algebraic Specifications
D. Lucanu, G. Ciobanu
We use hidden algebra as a formal framework for objectoriented paradigm. We introduce a labeled transition system for eachobject specification model, and then define a suitable notion ofbisimulation 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.We build a special CTL model directly from the object specification.Using this CTL model, we can verify the temporal properties using asoftware tool allowing SMV model checking.
A shorter version of the paper was accepted at the Fifth InternationalConference on Verification, Model Checking and Abstract Interpretation (VMCAI 2003).

TR0302 (2003) – MpNT: A MultiPrecision Number Theory Package. NumberTheoretic Algorithms (I)
F.L. Tiplea, S. Iftene, C. Hritcu, I. Goriac, R.M. Gordan, E. Erbiceanu
MpNT is a multiprecision number theorypackage 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 numbertheoretic 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 ComputerScience, 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 viewwe have tried to prepare a selfcontained 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.

TR0301 (2003) – Concurrent Composition of Objects in Hidden Logic
Dorel Lucanu
An operator __ for concurrent composition of objects specifiedin hidden logic is proposed and the main properties for this operatorare proved.

TR0206 (2002) – Transforming SelfEmbedded ContextFree Grammars into Regular Expressions
St.Andrei, S.Cavadini, WN. Chin
Our paper refers to the contextfree and regular languages. Wepoint out in an algorithmic manner using system of equationsthe situations when a contextfree grammar generates a regularlanguage: the case of oneletter alphabet and some cases ofselfembedded contextfree grammars.Moreover, we describe some other sufficient conditions when aselfembedded contextfree grammar generates a (non)regularlanguage. The paper proves that the systems of equations withselfembeddedness terms like XaX still have as solution a regularlanguage. In order to enlarge the class of contextfree grammarswhich generates regular languages, the class of oneletterfactorizable contextfree grammars is introduced.
Parts of this technical report have been published as follows:
1. Andrei, St., Cavadini, S.C., Chin, W.N.: A New Algorithmfor Regularizing OneLetter ContextFree Grammars. Theoretical Computer Science, Volume 306, Issues 13, pp. 113122 (2003)
2. Andrei, St., Chin, W.N., Cavadini, S.C.: Selfembedded contextfreegrammars with regular counterparts. Acta Informatica, Volume 40, Number 5, pp. 349365 (2004)

TR0205 (2002) – Coverability Structure Based Analysis
Roxana Melinte
Petri nets, vector addition systems,and parallel and communicating grammar systems are three basic theories formodeling and analysing parallel and distributed systems. The aim of this paper is to give an overviewon a basic technique of analysis which can beused for all three theories mentioned above.This technique is based on the reduction ofan infinite structure to a finite one, calledcoverability structure.By means of this technique, many decisionproblems can be discussed in an uniform way.

TR0204 (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 propertiescan be cleanly analysed.The aim of this paper is to give an overviewon the basic decision problems in the theoryof Petri nets. We discuss both decidability and complexity aspects.We have also a contribution in the area ofhome markings. We prove thatthe home marking problem for inhibitor Petrinets is undecidable.

TR0203 (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 accomplishthis matter. Among them the Petri net theoryplays an important role. This is because a Petri net model is a verysimple mathematical structure, but quite expressive. Basic properties of real systems, like safenessor boundedness, liveness, deadlockfreeness,the existence of home markings etc., can be cleanly modeled and analysed by means ofPetri nets. The aim of this paper is to give an overviewon safeness, liveness, deadlockfreeness andhome marking properties of Petri nets. As a contribution, we establish results provingconnections between the existence of home markings for confluent and noetherian Petrinets.

TR0202 (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 problemfor 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 existenceof home markings to confluence and noetherianity andprove that confluent and noetherian Petri nets havean unique home marking. Finally, we define some versions of the state space inclusion problem related to thehome marking and submarking problems, and discuss their decidability status.

TR0201 (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.
In this paper we generalize the properties of discreteness, observability, and generability byallowing 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, andthen investigate the relationships between various concepts ofcompleteness.

TR0101 (2001) – On ConcurrencyDegrees 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 concurrencydegrees 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 autoconcurrency, i.e. the case of a transition fireable simultaneously with itself at a marking. In this paper we give a more general definition of concurrencydegree for Petri nets and for jumping Petri nets, which takes into consideration also the autoconcurrency, for replacing the old definitions which ignore the autoconcurrency. Moreover, we show how we can compute these more general concurrencydegrees.

TR0001 (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.

TR9903 (1999) – WDS’99 The Scientific Programme and Communications
D. Lucanu, Gh. Stefanescu (editors)

TR9902 (1999) – Eurolan’99 (4th) Eurolan Summer School on Human Language Technology
D. Cristea et. al. (eds.)

TR9901 (1999) – On the Object Aggregation in CafeOBJ: Three Case Studies
Dorel Lucanu
Aggregation is the “partwhole” relationship in which objects representing the components are associated with a composite objectrepresenting the entire ensemble. In this paper we propose a methodology for specifying composite objects in algebraic specificationlanguages like CafeOBJ. We study three kinds of aggregation: aggregation of concurrent objects, aggregation of synchronizedobjects, 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.

TR9803 (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 noncoherent 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$.