Let T : X →X be a continuous map of a compact metric space X. A point x E X is called Banach recurrent point if for all neighborhood V of x, (n ∈ N : T^n(x) ∈ V} has positive upper Banach density. Denote by Tr...Let T : X →X be a continuous map of a compact metric space X. A point x E X is called Banach recurrent point if for all neighborhood V of x, (n ∈ N : T^n(x) ∈ V} has positive upper Banach density. Denote by Tr(T), W(T), QW(T) and BR(T) the sets of transitive points, weakly almost periodic points, quasi-weakly almost periodic points and Banach recurrent points of (X, T). If (X, T) has the specification property, then we show that every transitive point is Banach recurrent and O≠ W(T) n Tr(T) ≠ W*(T) ∩ Tr(T) ≠ QW(T) ∩ Tr(T) ≠ BR(T) ∩ Tr(T), in which W*(T) is a recurrent points set related to an open question posed by Zhou and Feng. Specifically the set Tr(T) M W*(T) / W(T) is residual in X. Moreover, we construct a point x E BR / QW in symbol dynamical system, and demonstrate that the sets W(T), QW(T) and BR(T) of a dynamical system are all Borel sets.展开更多
Let M be a smooth compact manifold and A be a compact invariant set. In this article, we prove that, for every robustly transitive set A, flA satisfies a Cl-genericstable shadowable property (resp., Cl-generic-stable...Let M be a smooth compact manifold and A be a compact invariant set. In this article, we prove that, for every robustly transitive set A, flA satisfies a Cl-genericstable shadowable property (resp., Cl-generic-stable transitive specification property or Cl-generic-stable barycenter property) if and only if A is a hyperbolic basic set. In particular, flA satisfies a Cl-stable shadowable property (resp., Cl-stable transitive specification property or Cl-stable barycenter property) if and only if A is a hyperbolic basic set. Similar results are valid for volume-preserving case.展开更多
Brillouin spectroscopy is an emerging tool for microscopic optical imaging as it allows for non-invasive and direct assessment of the viscoelastic properties of materials.Recent advances of background-free confocal Br...Brillouin spectroscopy is an emerging tool for microscopic optical imaging as it allows for non-invasive and direct assessment of the viscoelastic properties of materials.Recent advances of background-free confocal Brillouin spectrometer allows investigators to acquire the Brillouin spectra for turbid samples as well as transparent ones.However,due to strong signal loss induced by the imperfect optical setup,the Brillouin photons are usually immersed in background noise.In this report,we proposed and experimentally demonstrated multiple approaches to enhance the signal collction eficiency.A signal enhancement by>4 times can be observed,enabling ob-servation of ultra-weak signals.展开更多
Let X be a compact metric space and let f:X→X be an Anosov map,i.e.,an expansive selfmap with the pseudoorbit tracing property(abbr.POTP)(see Lemma 1).If Nn(f) denotes the number of fixed points of f^n which we name ...Let X be a compact metric space and let f:X→X be an Anosov map,i.e.,an expansive selfmap with the pseudoorbit tracing property(abbr.POTP)(see Lemma 1).If Nn(f) denotes the number of fixed points of f^n which we name here the n-periodic number then we prove in the case as n tends to infinity that n^M ≤N_n(f)≤H^n,where M and H are two positive integers.展开更多
We present a method and a tool for the verification of causal and temporal properties for embedded systems.We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware an...We present a method and a tool for the verification of causal and temporal properties for embedded systems.We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software.The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace.We propose a model-based approach that relies on domain specific languages(DSL).A first DSL,called TISL(trace item specification language),captures the relevant data structures.A second DSL,called STML(simulation trace mapping language),abstracts the simulation raw data into logical clocks,abstracting simulation data into relevant observation probes and thus reducing the trace streams size.The third DSL,called TPSL,defines a set of behavioral patterns that include widely used temporal properties.This is meant for users who are not familiar with temporal logics.Each pattern is transformed into an automata.All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated.The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve.We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes,thus reducing the verification time.展开更多
基金Supported by National Natural Science Foundation of China,Tian Yuan Special Foundation(Grant No.11426198)the Natural Science Foundation of Guangdong Province,China(Grant No.2015A030310166)
文摘Let T : X →X be a continuous map of a compact metric space X. A point x E X is called Banach recurrent point if for all neighborhood V of x, (n ∈ N : T^n(x) ∈ V} has positive upper Banach density. Denote by Tr(T), W(T), QW(T) and BR(T) the sets of transitive points, weakly almost periodic points, quasi-weakly almost periodic points and Banach recurrent points of (X, T). If (X, T) has the specification property, then we show that every transitive point is Banach recurrent and O≠ W(T) n Tr(T) ≠ W*(T) ∩ Tr(T) ≠ QW(T) ∩ Tr(T) ≠ BR(T) ∩ Tr(T), in which W*(T) is a recurrent points set related to an open question posed by Zhou and Feng. Specifically the set Tr(T) M W*(T) / W(T) is residual in X. Moreover, we construct a point x E BR / QW in symbol dynamical system, and demonstrate that the sets W(T), QW(T) and BR(T) of a dynamical system are all Borel sets.
基金supported by CAPES(Brazil)supported by National Natural Science Foundation(10671006,10831003)National Basic Research Program of China(973 Program)(2006CB805903)
文摘Let M be a smooth compact manifold and A be a compact invariant set. In this article, we prove that, for every robustly transitive set A, flA satisfies a Cl-genericstable shadowable property (resp., Cl-generic-stable transitive specification property or Cl-generic-stable barycenter property) if and only if A is a hyperbolic basic set. In particular, flA satisfies a Cl-stable shadowable property (resp., Cl-stable transitive specification property or Cl-stable barycenter property) if and only if A is a hyperbolic basic set. Similar results are valid for volume-preserving case.
基金supported by the start-up funds available through Texas A&M Universitysupport of the NIH (Grant#R21EB011703) and the NSF (ECCS Grant#10665620,DBI Grant#10665621 and CBET Grant#10665623).
文摘Brillouin spectroscopy is an emerging tool for microscopic optical imaging as it allows for non-invasive and direct assessment of the viscoelastic properties of materials.Recent advances of background-free confocal Brillouin spectrometer allows investigators to acquire the Brillouin spectra for turbid samples as well as transparent ones.However,due to strong signal loss induced by the imperfect optical setup,the Brillouin photons are usually immersed in background noise.In this report,we proposed and experimentally demonstrated multiple approaches to enhance the signal collction eficiency.A signal enhancement by>4 times can be observed,enabling ob-servation of ultra-weak signals.
文摘Let X be a compact metric space and let f:X→X be an Anosov map,i.e.,an expansive selfmap with the pseudoorbit tracing property(abbr.POTP)(see Lemma 1).If Nn(f) denotes the number of fixed points of f^n which we name here the n-periodic number then we prove in the case as n tends to infinity that n^M ≤N_n(f)≤H^n,where M and H are two positive integers.
基金supported by the Sino-European LIAM A Laboratory and by the INRIA Sophia Antipolis Research Center.
文摘We present a method and a tool for the verification of causal and temporal properties for embedded systems.We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software.The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace.We propose a model-based approach that relies on domain specific languages(DSL).A first DSL,called TISL(trace item specification language),captures the relevant data structures.A second DSL,called STML(simulation trace mapping language),abstracts the simulation raw data into logical clocks,abstracting simulation data into relevant observation probes and thus reducing the trace streams size.The third DSL,called TPSL,defines a set of behavioral patterns that include widely used temporal properties.This is meant for users who are not familiar with temporal logics.Each pattern is transformed into an automata.All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated.The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve.We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes,thus reducing the verification time.