হাইব্রিড সিস্টেম

একটি হাইব্রিড সিস্টেম এমন একটি গতিশীল ব্যবস্থা যা অবিচ্ছিন্ন (একটানা) এবং বিযুক্ত (পৃথক) উভয় ধরণের গতিশীল আচরণ প্রদর্শন করে। এটি এমন একটি ব্যবস্থা যা প্রবাহ (যা ডিফারেনশিয়াল সমীকরণ দ্বারা বর্ণিত) এবং লাফ (যা স্টেট মেশিন, অটোমেটন বা ডিফারেন্স সমীকরণ দ্বারা বর্ণিত) করতে পারে।^[১] প্রায়শই, "হাইব্রিড সিস্টেম" শব্দের পরিবর্তে "হাইব্রিড গতিশীল ব্যবস্থা" শব্দটি ব্যবহৃত হয়, যাতে এটি অন্যান্য "হাইব্রিড সিস্টেম" ধারণা থেকে আলাদা হয়, যেমন নিউরাল নেট এবং ফাজি লজিক এর সংমিশ্রণ বা বৈদ্যুতিক এবং যান্ত্রিক ড্রাইভলাইনের সংযোগ। হাইব্রিড সিস্টেম একটি বড় শ্রেণির ব্যবস্থা অন্তর্ভুক্ত করার সুবিধা প্রদান করে, যা গতিশীল ঘটনার মডেলিংয়ে আরও বেশি নমনীয়তা নিশ্চিত করে।

সাধারণভাবে, একটি হাইব্রিড সিস্টেমের অবস্থা সংজ্ঞায়িত হয় অবিচ্ছিন্ন চলক এর মান এবং একটি বিযুক্ত মোড দ্বারা। এই অবস্থা হয় অবিচ্ছিন্নভাবে প্রবাহ শর্ত অনুসারে পরিবর্তিত হয় অথবা কন্ট্রোল গ্রাফ অনুযায়ী বিযুক্তভাবে পরিবর্তিত হয়। অবিচ্ছিন্ন প্রবাহ অনুমোদিত হয় যতক্ষণ না তথাকথিত অবিচ্ছিন্ন শর্ত ( অপরিবর্তনীয় ) পূর্ণ হয়। অন্যদিকে, বিযুক্ত রূপান্তর ঘটতে পারে যখন নির্ধারিত লাফ শর্ত ( জাম্প অবস্থা ) পূরণ হয়। এই বিযুক্ত রূপান্তরগুলো কখনও কখনও ইভেন্ট এর সাথে সম্পর্কিত হতে পারে।

উদাহরণ

হাইব্রিড সিস্টেম বিভিন্ন সাইবার-ফিজিক্যাল সিস্টেম মডেল করতে ব্যবহৃত হয়েছে। এর মধ্যে রয়েছে ইমপ্যাক্ট সহ শারীরিক সিস্টেম, লজিক-ডায়নামিক কন্ট্রোলার, এবং ইন্টারনেট কনজেশন।

লাফানো বল

হাইব্রিড সিস্টেমের একটি সাধারণ উদাহরণ হল লাফানো বল, যা একটি ইমপ্যাক্ট-সম্পন্ন শারীরিক সিস্টেম। এখানে, বলটিকে (একটি পয়েন্ট-মাস হিসেবে ভাবা হয়) প্রাথমিক উচ্চতা থেকে ফেলে দেওয়া হয় এবং এটি মাটিতে আঘাত করে প্রতিবার লাফানোর সময় তার শক্তি ক্ষয় করে। বলটি প্রতিটি লাফের মধ্যে অবিচ্ছিন্ন গতিশীলতা প্রদর্শন করে; তবে, যখন এটি মাটিতে আঘাত করে, তখন এর বেগে একটি বিযুক্ত পরিবর্তন ঘটে যা অস্থিতিস্থাপক সংঘর্ষের মাধ্যমে মডেল করা হয়।

লাফানো বলের একটি গাণিতিক বর্ণনা নিম্নরূপ। ধরুন ${\displaystyle x_{1}}$ হল বলের উচ্চতা এবং ${\displaystyle x_{2}}$ হল বলের বেগ। বলকে বর্ণনা করা একটি হাইব্রিড সিস্টেম নিম্নরূপ:

যখন ${\displaystyle x\in C={x_{1}>0}}$, প্রবাহ দ্বারা নিয়ন্ত্রিত হয়: ${\displaystyle {\dot {x}}_{1}=x_{2},{\dot {x}}_{2}=-g}$, যেখানে ${\displaystyle g}$ হল মাধ্যাকর্ষণজনিত ত্বরণ। এই সমীকরণগুলি নির্দেশ করে যে বলটি মাটির ওপরে থাকলে, এটি মাধ্যাকর্ষণের কারণে মাটির দিকে টানতে থাকে।

যখন ${\displaystyle x\in D={x_{1}=0}}$, লাফ দ্বারা নিয়ন্ত্রিত হয়: ${\displaystyle x_{1}^{+}=x_{1},x_{2}^{+}=-\gamma x_{2}}$, যেখানে ${\displaystyle 0<\gamma <1}$ হল শক্তি ক্ষয়ের একটি ফ্যাক্টর। এটি নির্দেশ করে যে যখন বলের উচ্চতা শূন্য (বলটি মাটিতে আঘাত করেছে), তখন তার বেগ বিপরীত হয়ে যায় এবং ${\displaystyle \gamma }$ দ্বারা হ্রাস পায়। এটি কার্যত অস্থিতিস্থাপক সংঘর্ষের প্রকৃতি বর্ণনা করে।

লাফানো বল একটি বিশেষ আকর্ষণীয় হাইব্রিড সিস্টেম কারণ এটি জেনো আচরণ প্রদর্শন করে। জেনো আচরণের একটি কঠোর গাণিতিক সংজ্ঞা রয়েছে, তবে এটি অনানুষ্ঠানিকভাবে ব্যাখ্যা করা যায় যে সিস্টেমটি সীমিত সময়ে অসীম সংখ্যক লাফ দেয়। এই উদাহরণে, প্রতিবার বলটি লাফ দেয়, এটি শক্তি হারায়। ফলে, পরবর্তী লাফ (মাটির সাথে সংঘর্ষ) সময়ের সাথে ক্রমশ কাছাকাছি ঘটে।

উল্লেখযোগ্য যে গতিশীল মডেলটি সম্পূর্ণ হয় কেবল তখনই যখন মাটি এবং বলের মধ্যে সংস্পর্শ বল যোগ করা হয়। প্রকৃতপক্ষে, বল ছাড়া মডেলটি যথাযথভাবে সংজ্ঞায়িত করা যায় না এবং এটি যান্ত্রিক দৃষ্টিকোণ থেকে অর্থহীন। বল এবং মাটির মধ্যে মিথস্ক্রিয়া উপস্থাপন করার জন্য সবচেয়ে সহজ সংস্পর্শ মডেলটি হল বল এবং মাটির মধ্যে দূরত্ব (ফাঁক) এবং বলের সম্পর্কিত সংস্পর্শ বলের মধ্যে একটি পরিপূরক সম্পর্ক: ${\displaystyle 0\leq \lambda \perp x_{1}\geq 0.}$ এই সংস্পর্শ মডেলটি চুম্বকীয় বল বা গ্লুয়িং প্রভাব অন্তর্ভুক্ত করে না। যখন পরিপূরক সম্পর্কগুলো অন্তর্ভুক্ত করা হয়, তখন সংঘর্ষগুলো জমা হওয়ার এবং শেষ হওয়ার পরেও সিস্টেমটিকে ইন্টিগ্রেট করা যায়। সিস্টেমের স্থিতিশীল অবস্থা হল মাটির উপর বলের স্থিতিশীল অবস্থান। এখানে, মাধ্যাকর্ষণ এবং সংস্পর্শ বল ${\displaystyle \lambda }$ এর ক্রিয়াশীলতা একে স্থির রাখে।

বেসিক কনভেক্স বিশ্লেষণ থেকে বোঝা যায় যে পরিপূরক সম্পর্কটি একটি কনভেক্স সেটের সাথে একটি স্বাভাবিক শঙ্কুতে অন্তর্ভুক্তি হিসাবে পুনর্লিখন করা যেতে পারে। ফলে, লাফানো বলের গতিশীলতা একটি কনভেক্স সেটের স্বাভাবিক শঙ্কুর একটি ডিফারেনশিয়াল অন্তর্ভুক্তি হিসেবে কাজ করে।

হাইব্রিড সিস্টেমের যাচাইকরণ

হাইব্রিড সিস্টেমের বৈশিষ্ট্যগুলো স্বয়ংক্রিয়ভাবে প্রমাণ করার জন্য বিভিন্ন পদ্ধতি রয়েছে (যেমন, নিচে উল্লেখিত কিছু সরঞ্জাম)। হাইব্রিড সিস্টেমের নিরাপত্তা প্রমাণ করার সাধারণ কৌশলগুলোর মধ্যে রয়েছে পৌঁছানো সম্ভব এমন সেটগুলোর গণনা, অ্যাবস্ট্রাকশন রিফাইনমেন্ট, এবং ব্যারিয়ার সার্টিফিকেট।

তবে, বেশিরভাগ যাচাইকরণ কাজই অস্থির সিদ্ধান্তযোগ্য।^[২] এর ফলে, সাধারণ যাচাইকরণ অ্যালগরিদম ব্যবহার অসম্ভব। এর পরিবর্তে, বিভিন্ন সরঞ্জাম ব্যবহার করে পরীক্ষামূলক সমস্যাগুলোর উপর তাদের সক্ষমতা বিশ্লেষণ করা হয়।

এই বিষয়টির একটি তাত্ত্বিক বর্ণনা হতে পারে এমন অ্যালগরিদম যা হাইব্রিড সিস্টেম যাচাইকরণে প্রতিটি স্থিতিশীল ক্ষেত্রে সফল হয়।^[৩] এর অর্থ, যদিও অনেক সমস্যাই অস্থির সিদ্ধান্তযোগ্য, কিছু ক্ষেত্রে সেগুলো অন্তত কায়সিকভাবে সিদ্ধান্তযোগ্য।^[৪]

অন্যান্য মডেলিং পদ্ধতি

হাইব্রিড সিস্টেম মডেলিংয়ের জন্য দুটি মৌলিক পদ্ধতি রয়েছে। একটি হল আপাত বা স্পষ্ট (স্পষ্ট) পদ্ধতি এবং অন্যটি হল অন্তর্নিহিত বা অপ্রকাশিত (অন্তর্নিহিত ) পদ্ধতি। স্পষ্ট পদ্ধতিটি প্রায়শই হাইব্রিড অটোমেটন, একটি হাইব্রিড প্রোগ্রাম বা একটি হাইব্রিড পেট্রি নেট দিয়ে উপস্থাপিত হয়। অন্যদিকে, অন্তর্নিহিত পদ্ধতিটি প্রায়শই সুরক্ষিত সমীকরণ (সুরক্ষিত সমীকরণ) দ্বারা উপস্থাপিত হয় যা ডিফারেনশিয়াল বীজগণিত সমীকরণ (DAEs) এর সিস্টেম তৈরি করে। এখানে সক্রিয় সমীকরণ পরিবর্তিত হতে পারে, যেমন হাইব্রিড বন্ড গ্রাফের মাধ্যমে।

হাইব্রিড সিস্টেম বিশ্লেষণের জন্য একটি統 একক সিমুলেশন পদ্ধতি হল বিচ্ছিন্ন ইভেন্ট সিস্টেম স্পেসিফিকেশন DEVS আনুষ্ঠানিকতার উপর ভিত্তি করে একটি পদ্ধতি। এই পদ্ধতিতে ডিফারেনশিয়াল সমীকরণের ইন্টিগ্রেটরগুলোকে পারমাণবিক বিচ্ছিন্ন ইভেন্ট সিস্টেম স্পেসিফিকেশন DEVS মডেলে পরিমাণগত (পরিমাপ) করা হয়। এই পদ্ধতিগুলি সিস্টেম আচরণের ট্রেস তৈরি করে, যা ডিফারেনশিয়াল টাইম সিস্টেমের চেয়ে পৃথক ইভেন্ট সিস্টেমের মতো কাজ করে।

টেম্পোরাল লজিক এবং অন্যান্য যাচাইকরণ

C2E2: অ-রৈখিক হাইব্রিড সিস্টেম যাচাই করার সরঞ্জাম।

HyTech: হাইব্রিড সিস্টেমের জন্য মডেল চেকার।

HSolver: হাইব্রিড সিস্টেম যাচাইয়ের জন্য একটি টুল।

KeYmaera: হাইব্রিড সিস্টেমের জন্য তত্ত্ব প্রমাণকারী।

PHAVer: পলিহেড্রাল হাইব্রিড অটোমেটন যাচাইকরণের সরঞ্জাম।

S-TaLiRo: টেম্পোরাল লজিক স্পেসিফিকেশনের সাথে সামঞ্জস্য রেখে হাইব্রিড সিস্টেম যাচাইয়ের জন্য MATLAB টুলবক্স।

অন্যান্য

SCOTS: হাইব্রিড সিস্টেমের জন্য সঠিক-বাই-নকশা কন্ট্রোলার সিনথেসিস করার একটি টুল।

SpaceEx: স্টেট-স্পেস এক্সপ্লোরার।

তথ্যসূত্র

1. Branicky, Michael S. (২০০৫), Hristu-Varsakelis, Dimitrios; Levine, William S., সম্পাদকগণ, "Introduction to Hybrid Systems", Handbook of Networked and Embedded Control Systems (ইংরেজি ভাষায়), Boston, MA: Birkhäuser, পৃষ্ঠা 91–116, আইএসবিএন 978-0-8176-4404-8, ডিওআই:10.1007/0-8176-4404-0_5, সংগ্রহের তারিখ ২০২২-০৬-০৮ উদ্ধৃতি টেমপ্লেট ইংরেজি প্যারামিটার ব্যবহার করেছে (link)
2. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya: What's Decidable about Hybrid Automata, Journal of Computer and System Sciences, 1998
3. Martin Fränzle: Analysis of Hybrid Systems: An ounce of realism can save an infinity of states, Springer LNCS 1683
4. Stefan Ratschan: Safety verification of non-linear hybrid systems is quasi-decidable, Formal Methods in System Design, volume 44, pp. 71-90, 2014, ডিওআই:10.1007/s10703-013-0196-2

বহিঃসংযোগ

IEEE CSS কমিটি অন হাইব্রিড সিস্টেমস