# Robert Meolic

### Faculty of Electrical Engineering and Computer Science University of Maribor meolic@uni-mb.si

Here are my publications organized in CiteULike free service.
Here is my personal bibliography generated with COBISS (used by Slovenian libraries).
Here is BiBTeX file.

Here are publications cited in my Ph.D.

Journals:

Where not indicated, papers use english language.

1. Robert Meolic, Tomaz Dogša.
A C++ App for Demonstration of Sorting Algorithms on Mobile Platforms.
International Journal of Interactive Mobile Technologies, 8 (2014), 1 ; pages 40-45. -ISSN ***. [COBISS-ID ]
http://journals.sfu.ca/onlinejour/index.php/i-jim/article/view/3464

Abstract: This paper presents a systematic approach for designing a C++ app for demonstrating sorting algorithms on smartphones and tablets. It is part of an on-going project on the usages of new technologies in education. The general properties of mobile platforms are discussed together with details specific to demonstrating sorting algorithms. The implementation of Insertion Sort is given as an example. The obtained results (e.g. design rules and algorithms) have been tested within a prototype application.
Keywords: Usability, Qt, Engineering Education, Mobile learning

2. Robert Meolic.
Biddy - a multi-platform academic BDD package.
Journal of Software, 7 (2012), 6 ; pages 1358-1366. -ISSN 1796-217X. [COBISS-ID 16266006]
http://dx.doi.org/10.4304/jsw.7.6.1358-1366

Abstract: Biddy is a BDD package under GPL, developed at the University of Maribor. It uses ROBDDs with compleÂ­ment edges, as described in the paper K. S. Brace, R. L. Rudell, R. E. Bryant, Efficient Implementation of a BDD Package, 1990. Compared to other available BDD packages, Biddy's most distinguishing features are its specially deÂ­signed C interface and an original implementation of autoÂ­matic garbage collection. More generally, the Biddy project is not only concerned with the computer library, but also ofÂ­fers a demo application for the visualization of BDDs, called BDD Scout. The whole project is oriented towards a readÂ­able and comprehensible source code in C, which can be compiled unchanged on different platforms, including GNU/Linux and MS Windows.
Keywords: Boolean algebra, binary decision diagram, symbolic manipulation of Boolean functions, formal methÂ­ods, free software

3. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
ACTLW - An Action-based Computation Tree Logic With Unless Operator.
Information Sciences, 178 (2008), 6 ; pages 1542-1557. -ISSN 0020-0255. [COBISS-ID 12047638]
http://dx.doi.org/10.1016/j.ins.2007.10.023

Abstract: Model checkers for systems represented by labelled transition systems are not as extensively used as those for systems represented by Kripke structures. This is partially due to the lack of an elegant formal language for property specification which would not be as raw as, for example, HML yet also not as complex as, for example, $\mu$-calculus. This paper proposes a new action-based propositional branching-time temporal logic ACTLW, which enhances popular computation tree logic (CTL) with the notion of actions in a similar but more comprehensive way than action-based CTL introduced by R. De Nicola and F. Vaandrager in 1990. ACTLW is defined by using temporal operators until and unless only, whereas all other temporal operators are derived from them. Fixed-point characterisation of the operators together with symbolic algorithms for global model checking are shown. Usage of this new logic is illustrated by an example of verification of mutual-exclusion algorithms.
Keywords: formal verification, model checking, action-based temporal logic, fixed point, mutual-exclusion algorithm

4. Robert Meolic, Tatjana Kapus, Bogdan Dugonik, Zmago Brezočnik.
Formal verification of distributed mutual-exlusion circuits.
Inf. MIDEM, Ljubljana, 33 (2003), 3 ; pages 157-169. -ISSN 0352-9045. [COBISS-ID 8590614]
postscript, pdf.

Abstract: Distributed mutual-exclusion (DME) circuits are an interesting example of asynchronous circuits. They are composed of identical DME cells connected in a ring of arbitrary size. Each DME cell provides a connection point for one user, and all users compete for exclusive access to a shared resource. This paper reports about formal verification of two well-known DME circuit implementations. External behaviour of the circuits is described with a simple process, whereas the required properties are expressed with temporal logic ACTL. We were able to detect hazards and verify correctness of external behaviour of the circuits under the fundamental mode of operation.
Keywords: asynchronous circuit, fundamental mode, process algebra, model checking, ACTL

Some results in this paper needs revision. They have been partialy revised in Ph.D.

5. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Exploring properties of a bounded retransmission protocol with VIS.
CIT --- Journal of Computing and Information Technology, Zagreb, 7 (1999), 4 ; pages 311-321. -ISSN 1330-1136. [COBISS-ID 5341206]
postscript, pdf, CIT.

Abstract: It is of great interest for users of communication protocols to have a proof that they are correct and reliable to use. In order to prove a protocol correct formally, the protocol and the required properties must be formally described. This paper reports on verifying properties of a bounded retransmission protocol for large data packets. It is used to transfer les via a lossy communication channel. We emphasize timing properties of the protocol. We specied the protocol in Verilog and stated properties in a computation tree logic. The verication was carried out automatically by model checking. We used the non-commercial tool VIS which made it possible to introduce nondeterministic choice of data packets length and a realistic notion of time.
Keywords: formal verication, bounded retransmission protocol, model checking, CTL, Verilog, VIS

6. Ales Casar, Robert Meolic, Zmago Brezočnik, Bogomir Horvat.
Predstavitev logičnih funkcij z minimalnimi urejenimi binarnimi odločitvenimi grafi.
Elektrotehniski vestnik, Ljubljana, 59 (1992), 5 ; pages 299-307. -ISSN 0013-5852. [COBISS-ID 4599556].

Abstract: This paper describes data structures and algorithms for the representation of Boolean functions with reduced ordered binary decision diagrams (ROBDDs). A hash table is used for quick search. Additional information about variables and functions is stored in binary trees. Manipulations on functions are based on a recursive algorithm of ITE operation. The primary goal of this article is to describe programming technics needed to realize the idea. For the first time here recursive algorithms for composing functions and garbage collection with a formulae counter are presented. This is better than garbage collection in other known implementations. The results of the tests show that the described representation is very eficient in applications which operate with Boolean functions.
Keywords: boolean algebra, reduced ordered binary decision diagrams

The main results of this paper are also covered in paper "Representation of Boolean functions with ROBDDs" which has been presented at IEEE Region 8 Student Paper Contest, Paris-Evry, 1993.

Conference papers:

Where not indicated, papers use english language.

1. Uroš Berglez, Robert Meolic
Firefox OS: nov izziv za študentske projekte.
Twentythird International Electrotechnical and Computer Science Conference ERK'2014, Portoroz, Slovenia, volume B, pages 169-172, September 2014. [COBISS-ID ??]
pdf

Firefox OS: a new challenge for student projects
Abstract: Telecommunications students must carry out a number of projects while studying, and many of them involve mobile devices. This paper suggests that Firefox OS, a new mobile operating system, is a good platform for such projects. One of its interesting benefits is a fast learning curve because it builds on standardised web technologies, which are already familiar to many students. Moreover, using an open platform is an ideal choice for academic environments. This paper shows that one can make an interesting project in a few relatively easy steps without installing and learning complex environments. Some important aspects of project planning are also discussed and an example of a student project is given.

2. Robert Meolic
Demonstration of sorting algorithms on mobile platforms.
CSEDU 2013, Aachen, Germany, pages 136-141, May 2013. [COBISS-ID 16876054]
pdf

Abstract: This paper presents a systematic approach to the implementation of a mobile framework for demonstrating of sorting algorithms. Well-known corresponding projects are listed. The pseudo-code form is discussed, together with the graphical presentation of actions. A set of atomic operations that reveal the concept of sorting algorithms has been identified. Implementations of Gnome Sort, Insertion Sort, and Quicksort are given as a portable C-style code. The presented code has been tested within a prototype application on a modern smartphone. The project was oriented towards the usage in mobile learning systems.

3. Robert Meolic, Bogdan Dugonik
Uporaba FLTK pri poučevanju programiranja v C++.
Twentieth Electrotechnical and Computer Science Conference ERK'2011, Portoroz, Slovenia, volume B, pages 441-444, September 2011. [COBISS-ID 15445014]
pdf

Using FLTK in the course about C++ programming
Abstract: This paper gives three relatively short C++ programs. They demonstrate the building of a graphical user interface by using free cross-platform library FLTK. All three programs are described and can be useful for demonstration of the basic concepts of object-oriented programming. Indeed, when students master them, their knowledge and programming skills are good enough to understand and create complex object-oriented programs - and this is our main goal of teaching programming in the first year.

4. Robert Meolic, Tatjana Kapus
Notes on specifying systems in EST.
Fiftenth Electrotechnical and Computer Science Conference ERK'2006, Portoroz, Slovenia, volume B, pages 23-26, September 2006. [COBISS-ID 10751766]
pdf, slides: pdf

Abstract: EST is a tool for formal verication of systems. A system to be verified should be specified in a CCS-like syntax. CCS has been chosen because it is widely used in theoretical approaches due to a relatively small set of operators and nice laws valid for them. In this paper we make an overview of operators supported by EST. They can be classified into two groups: standard CCS operators and additional operators which we introduced to shorten specifications and to facilitate traslations from other formalisms.

5. Robert Meolic, Alessandro Fantechi, Stefania Gnesi.
Witness and Counterexample Automata for ACTL.
FORTE 2004, Madrid, Spain, pages 259-275, September 27-30, 2004. [COBISS-ID 9120534]
pdf

Abstract: Witnesses and counterexamples produced by model checkers provide a very useful source of diagnostic information. They are usually returned in the form of a single computation path along the model of the system. However, a single computation path is not enough to explain all reasons of a validity or a failure. Our work in this area is motivated by the application of action-based model checking algorithms to the test case generation for models formally specied with a CCS-like process algebra. There, only linear and nite witnesses and counterexamples are useful and for the given formula and model an ecient representation of the set of witnesses (counterexamples) explaining all reasons of validity (failure) is needed. This paper identies a fragment of an action-based computation tree logic (ACTL), that guarantee linear witnesses and counterexamples. For it, witness and counterexample automata are introduced, which are nite automata recognizing linear witnesses and counterexamples, respectively. An algorithm for generating such automata is given.

Some results in this paper needs revision. They has been already revised in Ph.D.

6. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Ogrodje paketa za avtomatsko resevanje logicnih ugank.
Proceedings of the twelfth International Electrotechnical and Computer Science Conference ERK 2003, Ljubljana, Slovenia, volume B, pages 455-458, ISSN 1581-4572, September 25-26, 2003. [COBISS-ID 8236822]
postscript, pdf, slides: ppt

A framework for automatic solving of logic riddles
Abstract: We study a sort of logic riddles given as a set of facts from which other facts must be derived. These problems, usually stated for entertainment, can be easily solved if there is only a small number of possible solutions. However, they become much more complex when the number of facts and possible solutions grows. The problem motivated us to think about a framework for automatic solving using computer. It is based on a propositional calculus. The most complex part of the system is parsing and understanding of the facts stated in a natural language as well as their transformation into mathematical formulae.

7. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
CTL and ACTL patterns.
EUROCON'2001, Bratislava, Slovak Republic, volume 2, pages 540-543, July 5-7, 2001. [COBISS-ID 6380566]
postscript, pdf, slides: ppt

Abstract: Model checking has become a widely used technique for verification of concurrent systems. However, its use is still much restricted to scientists with high mathematical education because temporal logic formulae are difficult to understand and even more difficult to create. Therefore, many projects have been started to find out how computers can help engineers in specifying system properties. This paper reports on using patterns of temporal logic formulae, which facilitate the usage of model checking.

Some results in this paper needs revision. They has been already revised in Ph.D.

8. Robert Meolic.
Looking for technical reports.
The Symposium Extra Skills for Young Engineers, Maribor, Slovenia, pages 35-38, October 18-20, 2000. [COBISS-ID 5754390]
postscript, pdf

Abstract: This paper is about technical reports, a special type of research papers, that are getting more and more popular source of scientific knowledge. Five most important search engines for locating technical reports are described. Some other sources of research papers on the Internet are mentioned, too. Reading the paper you can improve your skills to search for scientific knowledge significantly. This is also the main purpose of the paper.

This paper is a little bit outdated.

9. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
The Efficient Symbolic Tools Package.
8th International Conference Software, Telecommunications and Computer Networks (SoftCOM 2000), Split, Croatia, volume 1, pages 147-156, October 10-14, 2000. [COBISS-ID 5745686]
postscript, pdf

Abstract: Efficient Symbolic Tools (EST) is a software package for formal verification of concurrent systems. It appears as an educational project and has been entirely written in the Laboratory of Microcomputer Systems at the Faculty of Electrical Engineering and Computer Science in Maribor. The main purpose of our work was a study of algorithms that could serve for formal verification of complex protocols, which are used in computer and telecommunication networks.

This paper is a little bit outdated.

10. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Model Checking: A Formal Method for Safety Assurance of Logistic Systems.
2nd Congress Transport - Traffic - Logistics, Portoroz, Slovenia, pages 355-358, October 2-3, 2000. [COBISS-ID 5729814]
postscript, pdf, doc

Abstract: Model checking is a formal method widely used in computer science for verification of concurrent systems, e.g. communication protocols. The method requires that a system is given with a graph and properties of the system are given as a set of logic formulas. Model checking is an algorithmic method and it can be carried out fully automatically by fixpoint calculation. This paper describes how to use model checking for safety assurance of logistic systems.

11. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Reasoning about data in a simple process algebra.
Ninth Electrotechnical and Computer Science Conference ERK'2000, Portoroz, Slovenia, volume B, pages 19-22, September 2000. [COBISS-ID 5798422]
postscript, pdf

Abstract: Various process algebras have been introduced for reasoning about concurrent systems. Some of them include explicit data-passing mechanisms, while others do not. This paper presents a non-trivial problem involving data, which can also be comprehensively solved with a simple process algebra without explicit data-passing. The presented problem is very suitable for comparing the strength of different process algebra software tools.

Some results in this paper needs revision.

12. Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Computing testing equivalence with binary decision diagrams.
In Proceedings of the Seventh Electrotechnical and Computer Science Conference ERK'98, Baldomir Zajc, ed., Ljubljana, Slovenia Section IEEE, Portoroz, Slovenia, volume B, pages 51-54, September 1998.
[COBISS-ID 4007190] postscript, pdf slides: postscript, pdf

Abstract: Process algebras are a convenient tool for describing and reasoning about the behaviour of concurrent systems. A variety of equivalence relations are used to study the relationship between different systems or between different levels of abstractions of the system. This paper reports on an implementation of a testing equivalence with binary decision diagrams (BDDs). It is defined in terms of observations that process may or must satisfy. As the testing equivalence is shown to be an instance of a bisimulation equivalence, efficient algorithms for computing bisimulations using BDDs could be employed for its implementation.

13. Robert Meolic, Zmago Brezočnik.
Splosno razčlenitveno pravilo za OBDD, OFDD in 0-sup-BDD.
In Proceedings of the Fifth Electrotechnical and Computer Science Conference ERK'96, Baldomir Zajc, ed., Franc Solina, ed., Ljubljana, Slovenia Section IEEE, Portoroz, Slovenia, volume B, pages 11-14, September 1996. [COBISS-ID 2199318]
postscript, pdf slides: postscript, pdf

Universal decomposition rule for OBDD, OFDD, and 0-sup-BDD
Abstract: Binary decision diagrams (BDD) are very successful data structure for representation and manipulation of Boolean functions. Various types of BDDs have been proposed. In this paper relations between OBDD, OFDD, and 0-sup-BDD are shown in a new way. A generic decomposition rule for them is introduced. Using this rule a set of 288 types of BDDs is defined together with their reduction rules.

14. Robert Meolic, Zmago Brezočnik.
Predstavitev slik z binarnimi odločitvenimi grafi.
In Proceedings of the Fourth Electrotechnical and Computer Science Conference ERK'95, Franc Solina, ed., Baldomir Zajc, ed., Ljubljana, Slovenia Section IEEE, Portoroz, Slovenia, volume B, pages 111-114, September 1995. [COBISS-ID 7885316]
postscript, pdf

Representing Images with Binary Decision Diagrams
Abstract: This paper suggests binary decision diagram (BDD) as a useful data structure for representing images and image sequences. First, we give a short description of BDDs. Next, we show how they can be used to represent images. We perform some tests with bintrees and two common types of binary decision diagrams, ROBDDs and 0-sup-BDDs. Results show that BDDs are very efficient.

• Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
An Action Computation Tree Logic With Unless Operator,
Proceedings of the 1st South-East European workshop on formal methods SEEFM 2003, Thessaloniki, Greece, pages 100-114, November 20, 2003. [COBISS-ID 8430614]

This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.

• David Dedič, Robert Meolic.
Verification of Bakery algorithm variants for two processes.
Proceedings of the EUROCON 2003, Ljubljana, Slovenia, volume B, pages 35-39, September 22-24, 2003. [COBISS-ID 8241686]

This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.

• Robert Meolic, Tatjana Kapus, Ernest Gungl, Zmago Brezočnik.
Verification of mutual exclusion algorithms with EST.
Tenth Electrotechnical and Computer Science Conference ERK'2001, Portoroz, Slovenia, volume B, pages 15-18, September 24-26, 2001. [COBISS-ID 6540566]

This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.

• Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Verification of concurrent systems using ACTL.
In Applied informatics: proceedings of the IASTED international conference AI'2000, M. H. Hamza, ed., Anaheim, Calgary, ZÃ¼rich, IASTED/ACTA Press, Innsbruck, Austria, pages 663-669, February 14-17, 2000. [COBISS-ID 5347094]

This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.

• Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Specifikacija zahtev sistema z ACTL-jem.
In Proceedings of the Eight Electrotechnical and Computer Science Conference ERK'99, Baldomir Zajc, ed., Ljubljana, Slovenia Section IEEE, Portoroz, Slovenia, volume B, pages 23-26, September 1999. [COBISS-ID 483893]

This paper has been superseded. Its main results are covered in paper "ACTLW - An Action-based Computation Tree Logic With Unless Operator", Information Sciences, 2008.

• Robert Meolic, Tatjana Kapus, Zmago Brezočnik.
Verifying a Bounded Retransmission Protocol using VIS.
In Proceedings of the Sixth Electrotechnical and Computer Science Conference ERK'97, Baldomir Zajc, ed., Ljubljana, Slovenia Section IEEE, Portoroz, Slovenia, volume B, pages 15-18, September 1997. [COBISS-ID 3084310]

This paper has been superseded. Its main results are covered in paper "Exploring properties of a bounded retransmission protocol with VIS", CIT --- Journal of Computing and Information Technology, 1999.

Other

Where not indicated, papers use english language.

1. Ales Casar, Robert Meolic.
Representation of Boolean functions with ROBDDs.
Presented at IEEE Region 8 Student Paper Contest, Paris-Evry, 1993. [COBISS-ID 6992150]
postscript, pdf, slides: postscript, pdf

Abstract: This paper describes data structures and algorithms for the representation of Boolean functions with reduced ordered binary decision diagrams (ROBDDs). A hash table is used for quick search. Additional information about variables and functions is stored in binary trees. Manipulations on functions are based on a recursive algorithm of ITE operation. The primary goal of this article is to describe programming technics needed to realize the idea. For the first time here recursive algorithms for composing functions and garbage collection with a formulae counter are presented. This is better than garbage collection in other known implementations. The results of the tests show that the described representation is very eficient in applications which operate with Boolean functions. Keywords: boolean algebra, reduced ordered binary decision diagrams

Ph.D. thesis

• Robert Meolic,
Akcijska logika dreves izvajanj z operatorjem unless,
Ph.D. thesis, Faculty of Electrical Engineering and Computer Science Maribor, Slovenia, September 2005. [COBISS-ID 9981718]
pdf

An action-based computation tree logic with unless operator
Abstract: This thesis defines and studies action-based computation tree logic with {\em unless} operator (ACTLW). ACTLW is a propositional branching-time temporal logic. It is derived from logic ACTL, which was introduced in 1990 and which is one of established temporal logics for expressing properties of action-based models. ACTLW is more flexible than ACTL, because it does not impose the usage of silent action $\tau$ in expressing of the properties. ACTLW has also a slightly greater expressive power than ACTL, because it contains temporal operator {\em unless} ($\W$), whose meaning cannot be fully covered in ACTL. As opposite, all ACTL formulae can be expressed using ACTLW operators. ACTLW enables efficient implementation of model checking by using similar algorithms to those used for CTL model checking, which is a significant advantage in comparison to logic ACTL. The thesis gives a definition of logic ACTLW, derivations of all standard temporal operators, and algorithms for global ACTLW model checking using symbolic methods. Moreover, algorithms for generation of diagnostics for ACTLW, for generation of linear witnesses and counterexamples for ACTLW, and for generation of witness and counterexample automata for ACTLW are presented. The thesis is accomplished with patterns of ACTLW formulae and two larger practical examples: a verification of several different mutual-exclusion algorithms and a verification of two asynchronous distributed mutual-exclusion circuits.
Keywords: formal methods of system verification, model checking, temporal logic, CTL, ACTL, ACTLW, diagnostics, witness, counterexample, witness and counterexample automaton, mutual-exclusion problem

Master thesis

• Robert Meolic,
Preverjanje pravilnosti obnasanja sistemov s socasnostjo.
Master thesis, Faculty of Electrical Engineering and Computer Science Maribor, Slovenia, November 1999. [COBISS-ID 4972822]
postscript, pdf, dvi, slides: postscript, pdf

Checking correctness of concurrent systems behaviour
Abstract: This master thesis is about methods for checking correctness of concurrent systems behaviour based on the system specification with a process algebra. A definition of the process algebra and some examples of system specifications in terms of processes are given. The master thesis presents the checking of trace equivalence, strong, branching, and weak observational equivalence, testing equivalence, and symbolic model checking with propositional branching-time temporal logic ACTL. All discussed methods together form an efficient tool for formal verification of systems. An implementation of such a tool with BDDs is described. The usage of the tool is demonstrated on the verification of communication protocol BRP.
Keywords: formal methods of system verification, concurrent systems, process algebras, observational equivalences, testing equivalences, symbolic model checking, ACTL, BDD

Diploma work

• Robert Meolic,
Uporaba urejenih odlocitvenih grafov pri racunalniski obdelavi logicnih funkcij.
Diploma work, Faculty of Electrical Engineering and Computer Science Maribor, Slovenia, June 1995. [COBISS-ID 1821974]
slides: postscript, pdf

Using Ordered Decision Diagrams for Computer-Aided Manipulation of Boolean Functions
Abstract: Decision Diagrams are successful data structure for representation of Boolean functions. Mathematical background needed for their understanding and computer algorithms for their efficient implementation are given in this diploma work. Ordered Binary Decision Diagrams (OBDDs), Ordered Functional Decision Diagrams (OFDDs) and Zero-Suppresed Binary Decision Diagrams (0-sup-BDDs) are described in details. Also, a short overview of Free Binary Decision Diagrams (FBDDs), Extended Binary Decision Diagrams (XBDDs), Ordered Kronecker Functional Decision Diagrams (OKFDDs) and Differential Binary Decision Diagrams ($\triangle$BDDs) is included. For ROBDD, ROFDD, and 0-sup-BDD the decomposition rule and reduction rule are shown and algorithms for logical operations are derived. Algorithms were realized in programming language C. Efficiency of various types of decision diagrams is compared. Results of tests in the domains of Boolean function equality testing, representing combination sets, and representing images are given.
Keywords: Boolean algebra, Boolean functions, Binary Decision Diagrams, Functional Decision Diagrams, data structures