# Tehnical Reports

## TR 19-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 Ο(n

^{5}).## 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 Ο(n

^{6}).## 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 the**K**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 FCG

*light*) 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 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.

## TR07-02 (2007) – Secrecy for Security Protocols

**Catalin Birjoveanu**## TR07-01 (2007) – Secret Sharing Schemes with Applications in Security Protocols

**Sorin Iftene**## 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 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.

## TR05-07 (2005) – Embedding mobile ambients into the pi-calculus

**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 lambda-calculus, and the pi-calculus. In this paper wedemonstrate that we have a closer relationship between mobile ambients andthe pi-calculus. We present an embedding of pure mobile ambients into afragment of the pi-calculus, namely the localized sum-free synchronousmonadic pi-calculus with matching and mismatching. The embedding isachieved by associating a pair of localized pi-terms Structure_A and Rulerto every mobile ambient A. Structure_A simulates the spatial structure ofA by means of communication channels. Ruler is a universal pi-processintended to simulate the operational semantics of the mobile ambients.This embedding of pure mobile ambients into a subset of the pi-calculusopens new ways to the analysis of ambients by means of techniques used inthe pi-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 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%.

## 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 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.

## 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 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 random-search hybridization. We apply theseconcepts for the royal road fitness landscape. Experimentalresults indicate that Integrated-Adaptive Genetic Algorithms(IAGA) are particularly suited for tackling randomsearchhybridization. A learn-as-you-go system aimed at afine-grained 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.

## 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 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.

## 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 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, finite-sessions 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.

## 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 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.

## TR04-04 (2004) – Proprietati structurale ale retelelor Petri

**Cristian Vidrascu**## TR04-03 (2004) – Modular Analysis of Petri Net Models

**Aurora Tiplea**## TR04-02 (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.

## 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 amulti-agent 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 agent-oriented system(e.g., agents, hosts, name service, migration, and messaging).## 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 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).

## 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 anumber of applications, including the verification of timing constraintsforreal-time 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 well-knownrail-road crossing example, when its specification is being modified.

A concise and revised version of the paper was accepted at the10th IEEE Real-Time and Embedded Technology and Applications Symposium(RTAS 2004).

## 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 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).

## 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 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 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 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 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.

## TR03-01 (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.

## 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. Wepoint out in an algorithmic manner using system of equationsthe situations when a context-free grammar generates a regularlanguage: the case of one-letter alphabet and some cases ofself-embedded context-free grammars.Moreover, we describe some other sufficient conditions when aself-embedded context-free grammar generates a (non)regularlanguage. The paper proves that the systems of equations withself-embeddedness terms like XaX still have as solution a regularlanguage. In order to enlarge the class of context-free grammarswhich generates regular languages, the class of one-letterfactorizable 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 Algorithmfor 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-freegrammars with regular counterparts. Acta Informatica, Volume 40, Number 5, pp. 349-365 (2004)

## TR02-05 (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.

## 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 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.

## 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 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, deadlock-freeness,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, deadlock-freeness andhome marking properties of Petri nets. As a contribution, we establish results provingconnections between the existence of home markings for confluent and noetherian Petrinets.

## 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 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 sub-marking problems, and discuss their decidability status.

## 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.

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.

## 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]. 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.

## 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 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.## 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). 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$.