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.


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

Master thesis

Diploma work