A Generic Approach on How to Formally Specify and Model Check Path Finding Algorithms: Dijkstra, A* and LPA*

The paper describes how to formally specify three path finding algorithms in Maude, a rewriting logic-based programming/specification language, and how to model check if they enjoy desired properties with the Maude LTL model checker. The three algorithms are Dijkstra Shortest Path Finding Algorithm (DA), A* Algorithm and LPA* Algorithm. One desired property is that the algorithms always find the shortest path. To this end, we use a path finding algorithm (BFS) based on breadth-first search. BFS finds all paths from a start node to a goal node and the set of all shortest paths is extracted. We check if the path found by each algorithm is included in the set of all shortest paths for the property. A* is an extension of DA in that for each node [Formula: see text] an estimation [Formula: see text] of the distance to the goal node from [Formula: see text] is used and LPA* is an incremental version of A*. It is known that if [Formula: see text] is admissible, A* always finds the shortest path. We have found a possible relaxed sufficient condition. The relaxed condition is that there exists the shortest path such that for each node [Formula: see text] except for the start node on the path [Formula: see text] plus the cost to [Formula: see text] from the start node is less than the cost of any non-shortest path to the goal from the start. We informally justify the relaxed condition. For LPA*, if the relaxed condition holds in each updated version of a graph concerned including the initial graph, the shortest path is constructed. Based on the three case studies for DA, A* and LPA*, we summarize the formal specification and model checking techniques used as a generic approach to formal specification and model checking of path finding algorithms.

3D Shape Prediction of a Paper Model for a Brassiere Cup Consisting of Multiple Polygonal Patterns

A general method is proposed to predict the shape of a paper model of a brassiere cup. A brassiere cup consists of several cloth and wire parts and the shapes of cloth parts are determined by repeating creation of a paper cup model, check of its 3D shape, and modification of 2D shapes of parts. For efficient design of a brassiere cup, prediction of its 3D shape with a simulation is required. The deformed shape of a paper part is represented as a single or multiple developable surfaces. So, a model that can represent a part both as a single surface and as multiple surfaces is proposed. Which case is selected depends on the magnitude of the potential energy of the part in each case. The potential energy of the part and geometric constraints imposed on the part are formulated based on the model. Minimizing the potential energy under geometric constraints derives the stable shape of the part in either case. Furthermore, our proposed method can be applied to prediction of the paper cup model consisting of parts with complex shapes.

Is the d2 Test of Attention Rasch Scalable? Analysis With the Rasch Poisson Counts Model

The d2 test is a cancellation test to measure attention, visual scanning, and processing speed. It is the most frequently used test of attention in Europe. Although it has been validated using factor analytic techniques and correlational analyses, its fit to item response theory models has not been examined. We evaluated the fit of the d2 test to the Rasch Poisson Counts Model (RPCM) by examining the fit of six different scoring techniques. Only two scoring techniques—concentration performance scores and total number of characters canceled—fit the RPCM. The individual items fit the RPCM, with negligible differential item functioning across sex. Graphical model check and likelihood ratio test confirmed the overall fit of the two scoring techniques to RPCM.

Model Check What You Can, Runtime Verify the Rest

Model checking and runtime verification are pillars of formal verification but for the most part are used independently. In this position paper we argue that the formal verification community would be well-served by developing theory, algorithms, implementations, and applications that combine model checking and runtime verification into a single, seamless technology. This technology would allow system developers to carefully choose the appropriate balance between offline verification of expressive properties (model checking) and online verification of important parts of the system's state space (runtime verification). We present several realistic examples where such technology appears necessary and a preliminary formalization of the idea.