SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models DOI Creative Commons
Manuel Toscano-Moreno, Anthony Mandow, María Martínez

и другие.

Sensors, Год журнала: 2024, Номер 24(16), С. 5166 - 5166

Опубликована: Авг. 10, 2024

Linear temporal logic (LTL) formalism can ensure the correctness of mobile robot planning through concise, readable, and verifiable mission specifications. For uneven terrain, must consider motion constraints related to asymmetric slope traversability maneuverability. However, even though model checker tools like open-source Simple Promela Interpreter (SPIN) include search optimization techniques address state explosion problem, defining a global LTL property that encompasses both specifications on digital elevation models (DEMs) lead complex high computation times. In this article, we propose system incorporates set uncrewed ground vehicle (UGV) constraints, allowing these be omitted from checking. This is used in synthesizer for path planning, where an describes only specification. Furthermore, present specific parameterization synthesis using SPIN. We also offer two SPIN-efficient general formulas representative UGV missions reach DEM partition set, with specified or unspecified order, respectively. Validation experiments performed synthetic real-world DEMs demonstrate feasibility framework DEMs, achieving significant reduction cost compared baseline approach includes property, when applying appropriate planners.

Язык: Английский

A robust operators’ cognitive workload recognition method based on denoising masked autoencoder DOI
Xiaoqing Yu, Chun‐Hsien Chen

Knowledge-Based Systems, Год журнала: 2024, Номер 301, С. 112370 - 112370

Опубликована: Авг. 14, 2024

Язык: Английский

Процитировано

7

Tracking the Unseen and Unaware: Deciphering Controllers’ Detection Failures to Warnings Through Eye-Tracking Metrics DOI
Zhimin Li, Fan Li, Mengtao Lyu

и другие.

International Journal of Human-Computer Interaction, Год журнала: 2025, Номер unknown, С. 1 - 20

Опубликована: Янв. 13, 2025

Язык: Английский

Процитировано

1

Flashlight model: Integrating attention distribution and attention resources for pilots’ visual behaviour analysis and performance prediction DOI
Mengtao Lyu, Fan Li, Xingda Qu

и другие.

International Journal of Industrial Ergonomics, Год журнала: 2024, Номер 103, С. 103630 - 103630

Опубликована: Авг. 17, 2024

Язык: Английский

Процитировано

3

Flashlight Model: Integrating Attention Distribution and Attention Resources for Pilots' Visual Behaviour Analysis and Performance Prediction DOI
Mengtao Lyu, Fan Li, Xingda Qu

и другие.

Опубликована: Янв. 1, 2024

Pilot performance is almost the last line of defence in aircraft safety. Recent years have seen a surge research aimed at utilizing eye-tracking technology to predict pilot performance, enhancing aviation safety margins. A decline often attributed either misdirected attention towards irrelevant tasks or inefficient information processing owing limited resources. Previous has shown that data can effectively capture these issues and provide accurate predictions. Nevertheless, existing studies focus on distribution resources separately, ignoring complex interactions between them. To address this gap, our study proposes synthesized Flashlight model-based analysis for prediction, integrating two perspectives. Accordingly, combined AOI-gaze metrics are proposed offer more nuanced across specific Areas Interest (AOIs), thereby gaze metrics. We examined efficacy Gradient-boosted decision trees(GBDT) model prediction compared them with other widely used simulated flight experiment case study. Moreover, we employed SHapley Additive exPlanations (SHAP) method identify most influential measurements pilots' prediction. The result demonstrated selected obtained highest accuracy Overall, framework serve as systematic visual behaviour dynamic human-machine interactions.

Язык: Английский

Процитировано

0

SPIN-Based Linear Temporal Logic Path Planning for Ground Vehicle Missions with Motion Constraints on Digital Elevation Models DOI Creative Commons
Manuel Toscano-Moreno, Anthony Mandow, María Martínez

и другие.

Sensors, Год журнала: 2024, Номер 24(16), С. 5166 - 5166

Опубликована: Авг. 10, 2024

Linear temporal logic (LTL) formalism can ensure the correctness of mobile robot planning through concise, readable, and verifiable mission specifications. For uneven terrain, must consider motion constraints related to asymmetric slope traversability maneuverability. However, even though model checker tools like open-source Simple Promela Interpreter (SPIN) include search optimization techniques address state explosion problem, defining a global LTL property that encompasses both specifications on digital elevation models (DEMs) lead complex high computation times. In this article, we propose system incorporates set uncrewed ground vehicle (UGV) constraints, allowing these be omitted from checking. This is used in synthesizer for path planning, where an describes only specification. Furthermore, present specific parameterization synthesis using SPIN. We also offer two SPIN-efficient general formulas representative UGV missions reach DEM partition set, with specified or unspecified order, respectively. Validation experiments performed synthetic real-world DEMs demonstrate feasibility framework DEMs, achieving significant reduction cost compared baseline approach includes property, when applying appropriate planners.

Язык: Английский

Процитировано

0