Technical Reports

A List by Author: Radek Pelánek

e-mail:

xpelanek(a)fi.muni.cz

home page:

https://www.fi.muni.cz/~xpelanek

Evaluation of the Impact of Question Difficulty on Engagement and Learning

by Jan Papou¹ek, Vít Stanislav, Radek Pelánek, April 2016, 13 pages.

FIMU-RS-2016-02. Available as Postscript, PDF.

Abstract:

We study the impact of question difficulty on learners’ engagement and learning using an experiment with an open online educational system for adaptive practice of geography. The experiment shows that easy questions are better for short term engagement, whereas difficult questions are better for long term engagement and learning. These results stress the necessity of careful formalization of goals and optimization criteria of open online education systems. We also present disaggregation of overall results into specific contexts of practice and highlight the issue of attrition bias. This paper is an extended version of the paper presented at Intelligent Tutoring Systems conference.

Human Problem Solving: Sudoku Case Study

by Radek Pelánek, A full version of a paper presented at the 24th Florida Artificial Intelligence Research Society Conference January 2011, 21 pages.

FIMU-RS-2011-01. Available as Postscript, PDF.

Abstract:

We discuss and evaluate metrics for difficulty rating of Sudoku puzzles. The correlation coefficient with human performance for our best metric is 0.95. The data on human performance were obtained from three web portals and they comprise thousands of hours of human solving over 2000 problems. We provide a simple computational model of human solving activity and evaluate it over collected data. Using the model we show that there are two sources of problem difficulty: complexity of individual steps (logic operations) and structure of dependency among steps. Beside providing a very good Sudoku-tuned metric, we also discuss a metric with few Sudoku-specific details, which still provides good results (correlation coefficient is 0.88). Hence we believe that the approach should be applicable to difficulty rating of other constraint satisfaction problems. This technical report is a full version of a paper presented at the 24th Florida Artificial Intelligence Research Society Conference.

Human Problem Solving: Sokoban Case Study

by Petr Jaru¹ek, Radek Pelánek, April 2010, 25 pages.

FIMU-RS-2010-01. Available as Postscript, PDF.

Abstract:

We describe a case study in human problem solving for a particular problem - a Sokoban puzzle. For the study we collected data using the Internet. In this way we were able to collect significantly larger data (2000 problems solved, 780 hours of problem solving activity) than in typical studies of human problem solving. Our analysis of collected data focuses on the issue of problem difficulty. We show that there are very large differences in difficulty of individual Sokoban problems and that these differences are not explained by previous research. To address this gap in understanding we describe an abstract computational model of human problem solving, a metric of a problem decomposition, and formalization of a state space bottleneck. We discuss how these concepts help us understand human problem solving activity and differences in problem difficulty.

Verification Manager: Automating the Verification Process

by Radek Pelánek, Václav Rosecký, March 2009, 17 pages.

FIMU-RS-2009-02. Available as Postscript, PDF.

Abstract:

Although model checking is usually described as an automatic technique, the verification process with the use of model checker is far from being fully automatic. With the aim of automating the verification process, we elaborate on a concept of a verification manager. The manager automates some step of the verification process and enables efficient parallel combination of different verification techniques. We describe a realization of this concept for explicit model checking and discuss practical experience. Particularly, we discuss the problem of selection of input problems for evaluation of this kind of tool.

Evaluation of State Caching and State Compression Techniques

by Radek Pelánek, Václav Rosecký, Jaroslav ©edìnka, February 2008, 19 pages.

FIMU-RS-2008-02. Available as Postscript, PDF.

Abstract:

We study two techniques for reducing memory consumption of explicit model checking - state caching and state compression. In order to evaluate these techniques we review the literature, discuss trends in relevant research, and perform experiments over a large benchmark set (more than 100 models). The conclusion of our evaluation is that it is more important to combine several simple techniques in an appropriate way rather than to tune a single sophisticated technique.

Estimating State Space Parameters

by Radek Pelánek, Pavel ©imeèek, January 2008, 21 pages.

FIMU-RS-2008-01. Available as Postscript, PDF.

Abstract:

We introduce the problem of estimation of state space parameters, argue that it is an interesting and practically relevant problem, and study several simple estimation techniques. Particularly, we focus on estimation of the number of reachable states. We study techniques based on sampling of the state space and techniques that employ data mining techniques (classification trees, neural networks) over parameters of breadth-first search. We show that even through the studied techniques are not able to produce exact estimates, it is possible to obtain useful information about a state space by sampling and to use this information to automate the verification process.

Web Portal for Benchmarking Explicit Model Checkers

by Radek Pelánek, October 2006, 39 pages.

FIMU-RS-2006-03. Available as Postscript, PDF.

Abstract:

We present BEEM - BEnchmarks for Explicit Model checkers. This benchmark set includes more than 50 models together with correctness properties (both safety and liveness). The benchmark set is accompanied by an comprehensive web portal, which provides detailed information about all models. The web portal also includes information about state spaces and facilities selection of models for experiments.

The report describes the rationale beyond the form of the benchmark set, the design of the web portal and the main aspects of its realization, and also an example of an experimental analysis over the benchmark set: an analysis of a performance of sequential and distributed reachability.

The address of the web portal is http://anna.fi.muni.cz/models .

Reachability Relations and Sampled Semantics of Timed Systems

by Pavel Krèál, Radek Pelánek, A full version of the paper presented at conference FSTTCS 2005. December 2005, 31 pages.

FIMU-RS-2005-09. Available as Postscript, PDF.

Abstract:

Timed systems can be considered with two types of semantics -- dense time semantics and discrete time semantics. The most typical examples of both of them are real semantics and sampled semantics (i.e., discrete semantics with a fixed time step epsilon). In this work, we study different aspects of sampled semantics. At first, we study reachability relations between configurations of a timed automaton and provide a novel effective characterization of reachability relations. This result is used for proving our main result --- decidability of non-emptiness of a timed automaton omega-language in some sampled semantics (this problem was previously wrongly classified as undecidable). Also, we study relations between real semantics and sampled semantics with respect to different behavioral equivalences. Finaly, we study decidability of reachability problem for stopwatch automata with sampled semantics.

On-the-fly State Space Reductions

by Radek Pelánek, February 2005, 22 pages.

FIMU-RS-2005-03. Available as Postscript, PDF.

Abstract:

We present an overview of equivalences of finite state structures and discuss methods for computing reduced structures on-the-fly. We evaluate merits of these reductions on a large set of model checking case studies. It turns out that the achieved reduction can be significant, but that it is not so ``drastic" as sometimes claimed in the literature. We also propose some new reduction methods.

Deeper Connections between LTL and Alternating Automata

by Radek Pelánek, Jan Strejèek, September 2004, 26 pages.

FIMU-RS-2004-08. Available as Postscript, PDF.

Abstract:

It is known that Linear Temporal Logic (LTL) has the same expressive power as alternating 1-weak automata (A1W automata, also called alternating linear automata or very weak alternating automata). A translation of LTL formulae into a language equivalent A1W automata has been introduced in [MSS88]. The inverse translation has been developed independently in [Roh97] and [LT00]. We improve the latter translation and present deeper connections between LTL and A1W automata. Using these translations we identify the classes of A1W automata equivalent to LTL fragments given by bounds on nesting depths of temporal operators (see, e.g., [Wil99,KS02]) and the fragments of Until-Release hierarchy [CP03].

Relating Hierarchy of Linear Temporal Properties to Model Checking

by Ivana Èerná, Radek Pelánek, April 2003, 18 pages.

FIMU-RS-2003-03. Available as Postscript, PDF.

Abstract:

The hierarchy of properties as overviewed by Manna and Pnueli relates language, topology, omega-automata, and linear temporal logic classifications of properties. We provide new characterisations of this hierarchy in terms of automata with Buchi, co-Buchi, and Streett acceptance condition and in terms of Until-Release alternation hierarchy. Afterwards, we analyse the complex ity of the model checking problem for particular classes of the hierarchy and thanks to the new characterisations we identify those linear time temporal properties for which the model checking problem can be solved more efficiently than in the general case.

Distributed Explicit Fair Cycle Detection: Set Based Approach

by Ivana Èerná, Radek Pelánek, December 2002, 24 pages.

FIMU-RS-2002-09. Available as Postscript, PDF.

Abstract:

The fair cycle detection problem is at the heart of both LTL and fair CTL model checking. This paper presents a new distributed scalable algorithm for explicit fair cycle detection. Our method combines the simplicity of the distribution of explicitly presented data structure and the features of symbolic algorithm allowing for an efficient parallelisation. If a fair cycle (i.e. counterexample) is detected, then the algorithm produces a cycle, which is in general shorter than that produced by depth-first search based algorithms. Experimental results confirm that our approach outperforms that based on a direct implementation of the best sequential algorithm.

How to Employ Reverse Search in Distributed Single Source Shortest Paths

by Lubo¹ Brim, Ivana Èerná, Pavel Krèál, Radek Pelánek, This is a full version of the paper presented at SOFSEM 2001. November 2001, 22 pages.

FIMU-RS-2001-09. Available as Postscript, PDF.

Abstract:

A distributed algorithm for the single-source shortest path problem for directed graphs with arbitrary edge lengths is proposed. The new algorithm is based on relaxations and uses reverse search for inspecting edges and thus avoids using any additional data structures. At the same time the algorithm uses a novel way to recognize a reachable negative-length cycle in the graph which facilitates the scalability of the algorithm.

Distributed Shortest Paths for Directed Graphs with Negative Edge Lengths

by Lubo¹ Brim, Ivana Èerná, Pavel Krèál, Radek Pelánek, This is a full version of the paper presented at FST&TCS 2001. May 2001, 19 pages.

FIMU-RS-2001-01. Available as Postscript, PDF.

Abstract:

A distributed algorithm for single source shortest path problem in an arbitrary directed graph which can contain negative length cycles is presented. The new algorithm is a label-correcting one and uses a novel way for detection of negative length cycles. It works on a network of processors with disjoint memory that communicate via message passing. Correctness of the algorithm is proved. The algorithm is work-efficient as its worst time complexity is O(n^3/p), where p is the number of processors.