Formalizing Performance Evaluation of Mobile Manipulator Robots Using CTML

Computation Tree Measurement Language (CTML) is a newly developed formal language that offers simultaneous model verification and performance evaluation measures. CTML contains several advantages when compared to existing temporal logics. First, CTML can respond to nested queries with real-values or probabilities. Second, CTML can also express and respond to queries that are not supported by other existing logics, such as Probabilistic Computation Tree Logic (PCTL) or Probabilistic Linear Temporal Logic (PLTL). One example of this type of query is the survivability query, which asks how much time remains until a particular event occurs given that another event has already occurred. Finally, the runtime for responding to queries with CTML has been theoretically established to be polynomial with respect to the formula and input size. While the theory behind CTML has been established, the language has yet to be tested on a real-world example. In this work, we wish to demonstrate the utility of CTML when it is applied to a new field. To accomplish this, an artifact-based performance measurement methodology developed at the National Institute of Standards and Technology (NIST) was selected for modeling. The performance measurement method assesses mobile manipulator robots, which hold the potential to enable more flexible, dynamic workflows within manufacturing environments. Contributions of this work include the modeling of robot tasks implemented for the performance measurement test using Petri nets, as well as the formulation and execution of sample queries using CTML on models with varying sizes. The experimental procedure also included converting the Petri net model to a Discrete-Time Markov Chain (DTMC) using the Stochastic Model-Checking Analyzer for Reliability and Timing (SMART) tool and pairing the model with atomic functions so that it could be used as input for a software implementation of CTML. To demonstrate the advantages of CTML when compared to other temporal logics, the queries were re-formulated and evaluated using the PRISM Model Checker. This process required further adjustments to the model and rewards specification, in addition to the adjustment of program options, so that PRISM could be utilized to evaluate the model. In reporting our results and drawing comparisons, we interpret the numerical result of each query relative to the mobile manipulator performance measurement method, examine differences in the ease of implementation, and compare the empirical runtime between the two methods. We also accompany the queries that could not be re-translated into the logics supported by PRISM with an explanation. Finally, a discussion of future work is included, in which we consider how our findings could be extended relative to existing research in modeling the performance measurement method using Systems Modeling Language (SysML). This discussion also considers the integration of formal verification and SysML with Product Life-cycle (PLM) software solutions.