Author name cluster

Ivana Cerna

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

1 author row

ICRA Conference 2023 Conference Paper

Tentacle-Based Shape Shifting of Metamorphic Robots Using Fast Inverse Kinematics

Jan Mrázek
Patrick Ondika
Ivana Cerna
Jiri Barnat

We present a new approach to tackle the problem of metamorphic robots' reconfiguration. Given the chain-type metamorphic robot's initial and target configuration, we compute a reconfiguration plan that is provably physically collision-free. Our solution employs a specific heuristic. The robot initially reconfigures to a shape that resembles an octopus with many tentacles. After that, the tentacles gradually reconnect to each other using inverse kinematics, separating one tentacle from the body and keeping the other one connected. This strategy eventually leads to a snake-like structure of the robot. For the target configuration, we compute the reconfiguration plan with the same procedure, however, we reverse the plan to reconfigure the robot from the snake-like structure to the target shape. According to our experimental evaluation, our newly introduced strategy for finding reconfiguration plans is successful. It efficiently finds collision-free plans even for robots consisting of hundreds of modules.

Details

LPAR Conference 2020 Conference Paper

Rotation Based MSS/MCS Enumeration

Jaroslav Bendík
Ivana Cerna

Given an unsatisfiable Boolean Formula F in CNF, i. e. , a set of clauses, one is often interested in identifying Maximal Satisfiable Subsets (MSSes) of F or, equivalently, the complements of MSSes called Minimal Correction Subsets (MCSes). Since MSSes (MC- Ses) find applications in many domains, e. g. diagnosis, ontologies debugging, or axiom pinpointing, several MSS enumeration algorithms have been proposed. Unfortunately, finding even a single MSS is often very hard since it naturally subsumes repeatedly solving the satisfiability problem. Moreover, there can be up to exponentially many MSSes, thus their complete enumeration is often practically intractable. Therefore, the algorithms tend to identify as many MSSes as possible within a given time limit. In this work, we present a novel MSS enumeration algorithm called RIME. Compared to existing algorithms, RIME is much more frugal in the number of performed satisfiability checks which we witness via an experimental comparison. Moreover, RIME is several times faster than existing tools.

Details

LPAR Conference 2018 Conference Paper

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets

Jaroslav Bendík
Ivana Cerna

In many different applications we are given a set of constraints with the goal to decide whether the set is satisfiable. If the set is determined to be unsatisfiable, one might be interested in analysing this unsatisfiability. Identification of minimal unsatisfiable subsets (MUSes) is a kind of such analysis. The more MUSes are identified, the better insight into the unsatisfiability is obtained. However, the full enumeration of all MUSes is often intractable. Therefore, algorithms that identify MUSes in an online fashion, i. e. , one by one, are needed. Moreover, since MUSes find applications in various constraint domains, and new applications still arise, there is a desire for domain agnostic MUS enumeration approaches. In this paper, we present an experimental evaluation of four state-of-the-art domain agnostic MUS enumeration algorithms: MARCO, TOME, ReMUS, and DAA. The evalu- ation is conducted in the SAT, SMT, and LTL constraint domains. The results evidence that there is no silver-bullet algorithm that would beat all the others in all the domains.

Details

MFCS Conference 2003 Conference Paper

Relating Hierarchy of Temporal Properties to Model Checking

Ivana Cerna
Radek Pelánek

Abstract The hierarchy of properties as overviewed by Manna and Pnueli [18] relates language, topology, ω -automata, and linear temporal logic classifications of properties. We provide new characterisations of this hierarchy in terms of automata with Büchi, co-Büchi, and Streett acceptance condition and in terms of \(\Sigma^\mathit{LTL}_i\) and \(\Pi^\mathit{LTL}_i\) hierarchies. Afterwards, we analyse the complexity 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.

Details

MFCS Conference 1990 Conference Paper

Some Properties of Zerotesting Bounded One-Way Multicounter Machines

Ivana Cerna

Abstract Deterministic and nondeterministic one-way multicounter machines with bounds on the number of zerotests are studied. First, we establish a fine hierarchy of zerotesting bounded deterministic counter machine languages. Second, we show that a nondeterministic two-counter machine with 2 zerotests is able to recognize a language which cannot be accepted by any deterministic sublinear zerotesting bounded multicounter machine.

Details