Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Block Diagram Reduction01:22

Block Diagram Reduction

475
The process of deriving the transfer function of a control system often involves reducing its block diagram to a single block. This simplification can be achieved through a series of strategic operations, including relocating branch points and comparators. These operations preserve the overall function of the system while allowing for easier manipulation and combination of blocks.
The first step in this process is the identification and relocation of a branch point. A branch point, where a...
475
Theorems of Pappus and Guldinus: Problem Solving01:12

Theorems of Pappus and Guldinus: Problem Solving

1.0K
Pappus and Guldinus's theorems are powerful mathematical principles that are used for finding the surface area and volume of composite shapes. For example, consider a cylindrical storage tank with a conical top. Finding the surface area or volume can be challenging for such complex shapes. These theorems are particularly useful in calculating the volume and surface area of such systems. Here, the cylindrical storage tank with a conical top can be broken down into two simple shapes: a...
1.0K
Formal Charges02:42

Formal Charges

39.3K
In some cases, there are seemingly more than one valid Lewis structures for molecules and polyatomic ions. The concept of formal charges can be used to help predict the most appropriate Lewis structure when more than one reasonable structure exists.
39.3K
Relation between Mathematical Equations and Block Diagrams01:20

Relation between Mathematical Equations and Block Diagrams

2.8K
In a spring-mass-damper system, the second-order differential equation describes the dynamic behavior of the system. When transformed into the Laplace domain under zero initial conditions, this equation can be effectively analyzed and manipulated. The transformation into the Laplace domain converts differential equations into algebraic equations, simplifying the process of isolating the output.
2.8K
Constraints and Statical Determinacy01:26

Constraints and Statical Determinacy

911
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
911
Formulating and Validating Nursing Diagnosis I01:26

Formulating and Validating Nursing Diagnosis I

3.5K
A nursing diagnosis is written when the nurse recognizes a cluster of essential patient data indicating health problems treated with independent nursing interventions. The standardized terminologies of a nursing diagnosis help nurses identify and treat patients' problems. Every electronic health record that uses nursing diagnosis must employ standard diagnostic terminology. Developing an efficient, individualized care plan begins with accurate nursing diagnoses.
There are thirteen domains...
3.5K

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

SDHAR-HOME: A Sensor Dataset for Human Activity Recognition at Home.

Sensors (Basel, Switzerland)·2022
Same author

Efficient Path Planing for Articulated Vehicles in Cluttered Environments.

Sensors (Basel, Switzerland)·2020
Same author

A Waypoint Tracking Controller for Autonomous Road Vehicles Using ROS Framework.

Sensors (Basel, Switzerland)·2020
Same author

Implementing Autonomous Driving Behaviors Using a Message Driven Petri Net Framework.

Sensors (Basel, Switzerland)·2020

Related Experiment Video

Updated: Jan 3, 2026

RBDT: A Computerized Task System based in Transposition for the Continuous Analysis of Relational Behavior Dynamics in Humans
11:09

RBDT: A Computerized Task System based in Transposition for the Continuous Analysis of Relational Behavior Dynamics in Humans

Published on: July 17, 2021

3.3K

Formal Verification for Task Description Languages. A Petri Net Approach.

Joaquín López1, Alejandro Santana-Alonso1, Miguel Díaz-Cacho Medina1

  • 1Dep. Ingeniería de Sistemas y Automática, University of Vigo, 36200 Vigo, Spain.

Sensors (Basel, Switzerland)
|November 20, 2019
PubMed
Summary

This study introduces a novel method for verifying robotic systems by translating task-level control languages into Petri nets (PNs). This approach enhances the analysis of robotic system properties like liveness and deadlock-freeness.

Keywords:
autonomous robot systemformal verificationtask description languagetask-level programming

More Related Videos

Automation of a Positron-emission Tomography PET Radiotracer Synthesis Protocol for Clinical Production
10:20

Automation of a Positron-emission Tomography PET Radiotracer Synthesis Protocol for Clinical Production

Published on: October 26, 2018

11.8K
Functional Complementation Analysis FCA: A Laboratory Exercise Designed and Implemented to Supplement the Teaching of Biochemical Pathways
09:27

Functional Complementation Analysis FCA: A Laboratory Exercise Designed and Implemented to Supplement the Teaching of Biochemical Pathways

Published on: June 24, 2016

18.1K

Related Experiment Videos

Last Updated: Jan 3, 2026

RBDT: A Computerized Task System based in Transposition for the Continuous Analysis of Relational Behavior Dynamics in Humans
11:09

RBDT: A Computerized Task System based in Transposition for the Continuous Analysis of Relational Behavior Dynamics in Humans

Published on: July 17, 2021

3.3K
Automation of a Positron-emission Tomography PET Radiotracer Synthesis Protocol for Clinical Production
10:20

Automation of a Positron-emission Tomography PET Radiotracer Synthesis Protocol for Clinical Production

Published on: October 26, 2018

11.8K
Functional Complementation Analysis FCA: A Laboratory Exercise Designed and Implemented to Supplement the Teaching of Biochemical Pathways
09:27

Functional Complementation Analysis FCA: A Laboratory Exercise Designed and Implemented to Supplement the Teaching of Biochemical Pathways

Published on: June 24, 2016

18.1K

Area of Science:

  • Robotics
  • Formal Methods
  • Software Engineering

Background:

  • Verifying autonomous robotic systems is challenging due to asynchronous interactions and imperfect sensor data.
  • Task-level control in robots often relies on specialized languages.
  • Existing verification methods may require complex system-specific formalisms.

Purpose of the Study:

  • To present an effective approach for applying formal verification to robot control languages.
  • To avoid the need for modeling robotic systems in specific formalisms.
  • To enable the integration of formal verification into the software development cycle for robotic applications.

Main Methods:

  • Translating task-level control models into a Petri net (PN) based representation.
  • Developing new methods to analyze task properties such as liveness, deadlock-freeness, and terminability.
  • Utilizing the Petri Net Markup Language (PNML) for interoperability with existing PN tools.

Main Results:

  • The approach was successfully applied to the Task Description Language (TDL).
  • Experimental results demonstrate the effectiveness of the PN-based verification method.
  • The method provides a way to analyze critical task properties without direct system modeling.

Conclusions:

  • Formal verification of robotic task-level control languages is feasible using Petri nets.
  • The TDL to PN translation offers a practical pathway for enhancing robotic system reliability.
  • The goal is to develop tools for seamless integration of formal verification into robotic software development.