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

Relation between Mathematical Equations and Block Diagrams01:20

Relation between Mathematical Equations and Block Diagrams

161
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.
161
Block Diagram Reduction01:22

Block Diagram Reduction

152
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...
152
Simplified Synchronous Machine Model01:30

Simplified Synchronous Machine Model

173
The Synchronous Machine Model is a fundamental tool in analyzing and ensuring the transient stability of power systems. This model simplifies the representation of a synchronous machine under balanced three-phase positive-sequence conditions, assuming constant excitation and ignoring losses and saturation. The model is pivotal for understanding the behavior of synchronous generators connected to a power grid, particularly during transient events.
In this model, each generator is connected to a...
173
BIBO stability of continuous and discrete -time systems01:24

BIBO stability of continuous and discrete -time systems

324
System stability is a fundamental concept in signal processing, often assessed using convolution. For a system to be considered bounded-input bounded-output (BIBO) stable, any bounded input signal must produce a bounded output signal. A bounded input signal is one where the modulus does not exceed a certain constant at any point in time.
To determine the BIBO stability, the convolution integral is utilized when a bounded continuous-time input is applied to a Linear Time-Invariant (LTI) system....
324
Classification of Systems-I01:26

Classification of Systems-I

167
Linearity is a system property characterized by a direct input-output relationship, combining homogeneity and additivity.
Homogeneity dictates that if an input x(t) is multiplied by a constant c, the output y(t) is multiplied by the same constant. Mathematically, this is expressed as:
167
SFG Algebra01:16

SFG Algebra

100
In Signal Flow Graph (SFG) algebra, the value a node represents is determined by the sum of all signals entering that node. This summed value is then transmitted through every branch leaving the node, making the SFG a powerful tool for visualizing and analyzing control systems.
Each node in an SFG corresponds to a variable, and the interactions between nodes are represented by branches with associated gains. When multiple branches lead into a node, the value at that node is the sum of the...
100

You might also read

Related Articles

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

Sort by
Same author

[Prevalence and prognostic factors for postoperative complications of uvulopalatopharyngoplasty in patients with obstructive sleep apnea hypopnea syndrome].

Lin chuang er bi yan hou tou jing wai ke za zhi = Journal of clinical otorhinolaryngology head and neck surgery·2008
Same author

[Transurethral electrotomy for cystis vesicular seminalis induced by obstruction of the distal end of the ejaculatory duct].

Zhonghua nan ke xue = National journal of andrology·2008
Same author

[Effects of testosterone on the proliferation of rat corpus cavernosum cells in vitro].

Zhonghua nan ke xue = National journal of andrology·2008
Same author

Identification of 4-aminopyrazolylpyrimidines as potent inhibitors of Trk kinases.

Journal of medicinal chemistry·2008
Same author

Increased dialysate levels of phospholipids containing unsaturated fatty acid are associated with increased peritoneal transport rate.

American journal of nephrology·2008
Same author

Stepwise increase in the prevalence of isolated systolic hypertension with the stages of chronic kidney disease.

Nephrology, dialysis, transplantation : official publication of the European Dialysis and Transplant Association - European Renal Association·2008

Related Experiment Video

Updated: May 25, 2025

Closed-loop Neuro-robotic Experiments to Test Computational Properties of Neuronal Networks
11:18

Closed-loop Neuro-robotic Experiments to Test Computational Properties of Neuronal Networks

Published on: March 2, 2015

10.2K

Neural transition system abstraction for neural network dynamical system models and its application to Computational

Yejiang Yang1, Tao Wang2, Weiming Xiang3

  • 1School of Computer and Cyber Sciences, Augusta University, Augusta GA 30912, USA; School of Electrical Engineering, Southwest Jiaotong University, Chengdu, China.

Neural Networks : the Official Journal of the International Neural Network Society
|February 25, 2025
PubMed
Summary

This study introduces an explainable abstraction-based verification method for neural networks. It enhances model interpretability and enables formal verification using Computational Tree Logic (CTL).

Keywords:
CTL specificationData-driven modelingModel abstractionModel verificationReachability analysisTransition system

More Related Videos

Designing and Implementing Nervous System Simulations on LEGO Robots
10:34

Designing and Implementing Nervous System Simulations on LEGO Robots

Published on: May 25, 2013

15.0K
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

2.9K

Related Experiment Videos

Last Updated: May 25, 2025

Closed-loop Neuro-robotic Experiments to Test Computational Properties of Neuronal Networks
11:18

Closed-loop Neuro-robotic Experiments to Test Computational Properties of Neuronal Networks

Published on: March 2, 2015

10.2K
Designing and Implementing Nervous System Simulations on LEGO Robots
10:34

Designing and Implementing Nervous System Simulations on LEGO Robots

Published on: May 25, 2013

15.0K
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

2.9K

Area of Science:

  • Computer Science
  • Artificial Intelligence
  • Formal Methods

Background:

  • Data-driven models, particularly neural networks, often lack interpretability.
  • Formal verification methods are crucial for ensuring system reliability and safety.
  • Existing verification techniques may struggle with the complexity of neural network dynamics.

Purpose of the Study:

  • To propose an explainable abstraction-based verification method for neural network models.
  • To enhance the interpretability and user interaction in the verification process.
  • To enable formal verification of system behavior against specifications.

Main Methods:

  • State space partitioning using a data-driven process to abstract system dynamics.
  • Employing set-valued reachability analysis to estimate subsystem relationships.
  • Constructing a neural transition system abstraction from the neural network model.
  • Verifying the abstracted model using Computational Tree Logic (CTL).

Main Results:

  • The proposed method successfully abstracts complex system dynamics into understandable state labels.
  • Formal verification of neural network models is achieved through the constructed abstraction.
  • The framework demonstrates enhanced interpretability and validation capabilities.
  • Examples with Maglev and handwritten models illustrate the framework's effectiveness.

Conclusions:

  • The developed abstraction-based verification method significantly improves the interpretability of data-driven models.
  • The framework provides a robust approach for formal verification of neural network behavior using CTL.
  • This method facilitates validating complex systems against user-specified properties.