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.